runtimeverification / runtimeverification/haskell-backend
Evaluate `sat.smt=true` option for z3
@jberthold is already working on this.
Since Jan 28, 2025.
- Dominant language
- Haskell
- Stars
- 224
- Forks
- 43
- PR merge metrics
- No merged PRs in 30d
Description
Related: https://github.com/Z3Prover/z3/issues/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=trueoption - (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=trueoption used to slow down Z3 operations.
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.