METADATA
# LHS
Ramon benchmark for Z3
-
Job description: quotient_pairs=true inputs/certora2
Job tag: fix_in_qp_true_certora2
Runner: lev-ripper
Z3 repo: Z3Prover/z3
Z3 commit: 186ef6a0cd3f0fc8821795515994089cfc4e65db
Z3 branch: modgb
Z3 options: "-T:200 smt.arith.nl.grobner_quotient_pairs=true"
Z3 inputs: inputs/certora2
Z3 commit message: fix unsound grobner-quotient-pair lemma: skip lc with non-integral coefficients
pdd::reduce() can introduce non-integral coefficients via leading-term
division. The quotient lemma reasoning assumed lc_comb = lc_i - lc_j
was always integer-valued, which failed when lc had non-integral coefficients.
Filter out such entries when building var_to_facts.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
# RHS
Ramon benchmark for Z3
-
Job description: quotient_pairs=true inputs/certora2
Job tag: fix_in_qp_true_certora2
Runner: lev-ripper
Z3 repo: Z3Prover/z3
Z3 commit: 186ef6a0cd3f0fc8821795515994089cfc4e65db
Z3 branch: modgb
Z3 options: "-T:200 smt.arith.nl.grobner_quotient_pairs=true"
Z3 inputs: inputs/certora2
Z3 commit message: fix unsound grobner-quotient-pair lemma: skip lc with non-integral coefficients
pdd::reduce() can introduce non-integral coefficients via leading-term
division. The quotient lemma reasoning assumed lc_comb = lc_i - lc_j
was always integer-valued, which failed when lc had non-integral coefficients.
Filter out such entries when building var_to_facts.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>