Does Z3py support Linear Temporal logic LTL?

Question

Does Z3py support Linear Temporal logic LTL? If yes, can you provide an example of simple explain.

Answer 1

Z3 does not support LTL or other temporal or modal logics. The input accepted by Z3 is first-order logic with theories, such as arithmetic.