METADATA
# LHS
Ramon benchmark for Z3
-
Job description:
Job tag: smt-60-clausal-lookahead-sequential-qfnia-sat
Z3 repo: https://github.com/Z3Prover/z3
Z3 commit: 7fb6497ce1162635e7e5f78fe35bf4d5b02d2dbd
Z3 branch: master
Z3 options: "-T:60 -v:2 -st tactic.default_tactic="(then simplify propagate-values solve-eqs simplify smt)" smt.sls.enable=true smt.sls.parallel=false model_validate=true sls.arith_use_clausal_lookahead=true"
Z3 inputs: inputs/QF_UFNIA_SAT
Z3 commit message: fix return value when in external mode bool-flip
return null_bool_var instead of false (= 0).
# RHS
Ramon benchmark for Z3
-
Job description:
Job tag: smt-60-clausal-lookahead-sequential-qfnia-sat
Z3 repo: https://github.com/Z3Prover/z3
Z3 commit: 7fb6497ce1162635e7e5f78fe35bf4d5b02d2dbd
Z3 branch: master
Z3 options: "-T:60 -v:2 -st tactic.default_tactic="(then simplify propagate-values solve-eqs simplify smt)" smt.sls.enable=true smt.sls.parallel=false model_validate=true sls.arith_use_clausal_lookahead=true"
Z3 inputs: inputs/QF_UFNIA_SAT
Z3 commit message: fix return value when in external mode bool-flip
return null_bool_var instead of false (= 0).