METADATA
# LHS
Ramon benchmark for Z3
-
Job description:
Job tag: smt-10-alive-int-blast
Z3 repo: https://github.com/Z3Prover/z3
Z3 commit: 1ce6e66ac9b73e57ad93be95fa7797e4b1588c3e
Z3 branch: master
Z3 options: "-T:10 -v:2 -st tactic.default_tactic="(then simplify propagate-values solve-eqs simplify smt)" smt.bv.solver=2 model_validate=true "
Z3 inputs: inputs/alive-arm-tv-smt-benchmarks
Z3 commit message: generalize logic detection to use sub-string matching
# RHS
Ramon benchmark for Z3
-
Job description:
Job tag: smt-10-alive-int-blast
Z3 repo: https://github.com/Z3Prover/z3
Z3 commit: 1ce6e66ac9b73e57ad93be95fa7797e4b1588c3e
Z3 branch: master
Z3 options: "-T:10 -v:2 -st tactic.default_tactic="(then simplify propagate-values solve-eqs simplify smt)" smt.bv.solver=2 model_validate=true "
Z3 inputs: inputs/alive-arm-tv-smt-benchmarks
Z3 commit message: generalize logic detection to use sub-string matching