Evaluate `sat.smt=true` option for z3
@jberthold ci sta già lavorando.
Dal 28/1/2025.
Valutazione
Questa issue non è ancora stata valutata.
Descrizione
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.
- Lingua principale
- Haskell
- Stelle
- 228
- Fork
- 46
- Merge medio
- 21h 48m
- PR unite (30g)
- 1
Preparare l'ambiente
- Nessun Dockerfile né file Docker Compose
- Ha un modello di pull request
- Nessuna guida per i contributori
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Altre issue di runtimeverification/haskell-backend
-
Booster: Optimize KMap internal data structure to improve Map operation performanceForse di nuovo libera @Stevengre l’ha presa 245 giorni fa e non c’è nessuna pull request aperta. Aperta
runtimeverification/haskell-backend#4138 · 9 commenti · 1 assegnatario ·
-
Difficoltà 3/5 1-2 giorni Idoneità per principianti 48/100
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 38/100
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 35/100
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100
runtimeverification/haskell-backend#4112 · 2 commenti ·
Tutte le issue di runtimeverification/haskell-backend
Issue simili
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 64/100
I maintainer di solito rispondono entro 1 giorno
-
Difficoltà 1/5 Meno di un'ora Idoneità per principianti 95/100
objectionary/phino#2137 ·
I maintainer di solito rispondono entro 1 giorno
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 65/100
fmidue/logic-tasks#387 ·
-
enhancement
Difficoltà 2/5 1-3 ore Idoneità per principianti 78/100
alunduil/network-arbitrary#218 ·
I maintainer di solito rispondono entro 1 giorno
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 76/100
iand675/hs-opentelemetry#323 ·