1

I build the formula in z3 using the java API. However, I have some formula that are difficult to solve, and I want to investigate why. Therefore, I want to print the formula in SMTLIB2 format.

Is it possible to get that from a Solver object. Currently, what I can get is only an array of assertions. Thank you.

1 Answer 1

2

Yes, Solver.toString() does that. This should also include the variable/constant declarations if you are using the latest master; I think that part was added after the last release.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.