Related: Z3Prover/z3#7507
We have a test suite-produced script timeout-4.13.4.smt2.txt that times out with z3 v4.13.4 in the ite statement evaluation.
In the issue we opened in the z3 repository, sat.smt=true was recommended as a way to avoid this issue. Adding the option in haskell backend/booster by @jberthold caused the prover to loop and the = sign to be missing in the output.
The legacy backend does not use smtlib-backends-process (directly uses System.Process) and does not seem to have this problem.
- Investigate why the solver cannot be used by booster with the
sat.smt=true option
- (We already have a CLI option to pass options to the SMT solver). Test what happens when passing the option via CLI.
- Once the solver can be started and used with this option: Evaluate performance impact of the option. @PetarMax mentioned that this
sat.smt=true option used to slow down Z3 operations.
Related: Z3Prover/z3#7507
We have a test suite-produced script timeout-4.13.4.smt2.txt that times out with z3
v4.13.4in theitestatement evaluation.In the issue we opened in the z3 repository,
sat.smt=truewas recommended as a way to avoid this issue. Adding the option in haskell backend/booster by @jberthold caused the prover to loop and the=sign to be missing in the output.The legacy backend does not use
smtlib-backends-process(directly usesSystem.Process) and does not seem to have this problem.sat.smt=trueoptionsat.smt=trueoption used to slow down Z3 operations.