METADATA
# LHS
Ramon benchmark for Z3
-
Job description:
Job tag: smt_qfrdl-sequential
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: 477a1d817da44f7615fa53a10b4bd03d2cc84e48
Z3 branch: master
Z3 options: "-T:60 smt.threads=1 tactic.default_tactic=smt smt.auto_config=false"
Z3 inputs: inputs/QF_RDL
Z3 commit message: Add mod-factor-propagation lemma to NLA divisions solver (#9235)
When a monic x*y has a factor x with mod(x, p) = 0 (fixed), propagate
mod(x*y, p) = 0. This enables Z3 to prove divisibility properties like
x mod p = 0 => (x*y) mod p = 0, which previously timed out even for
p = 2. The lemma fires in the NLA divisions check and allows Gröbner
basis and LIA to subsequently derive distributivity of div over addition.
Extends division tuples from (q, x, y) to (q, x, y, r) to track the
mod lpvar. Also registers bounded divisions from the mod internalization
path in theory_lra, not just the idiv path.
Co-authored-by: Claude Opus 4.6 (1M context)
# RHS
Ramon benchmark for Z3
-
Job description:
Job tag: smt_qfrdl-sequential
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: 477a1d817da44f7615fa53a10b4bd03d2cc84e48
Z3 branch: master
Z3 options: "-T:60 smt.threads=1 tactic.default_tactic=smt smt.auto_config=false"
Z3 inputs: inputs/QF_RDL
Z3 commit message: Add mod-factor-propagation lemma to NLA divisions solver (#9235)
When a monic x*y has a factor x with mod(x, p) = 0 (fixed), propagate
mod(x*y, p) = 0. This enables Z3 to prove divisibility properties like
x mod p = 0 => (x*y) mod p = 0, which previously timed out even for
p = 2. The lemma fires in the NLA divisions check and allows Gröbner
basis and LIA to subsequently derive distributivity of div over addition.
Extends division tuples from (q, x, y) to (q, x, y, r) to track the
mod lpvar. Also registers bounded divisions from the mod internalization
path in theory_lra, not just the idiv path.
Co-authored-by: Claude Opus 4.6 (1M context)