mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

Fix non-termination in mod rewriter for symbolic modulus (issue #7403)

Browse source 
Add two rewrite rules in mk_mod_core:
1. mod(a + k*y, y) → mod(a, y): removes summands equal to (or integer multiples
   of) the symbolic modulus. Valid for all y including y=0 since k*0=0.
2. mod(mod(x, y), y) for symbolic y: rewrites via ite to terminate the
   E-matching chain created by the quantifier idempotency rule.

Also add regression tests in src/test/arith_rewriter.cpp covering both new rules.
This commit is contained in:
copilot-swe-agent[bot] 2026-07-13 04:30:49 +00:00 • committed by GitHub
parent 6bff306066
commit b544f7e58c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 69 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/test/arith_rewriter.cpp
View file

@ -83,4 +83,23 @@ void tst_arith_rewriter() {
rw(fml);
std::cout << "consecutive product (minus) >= 0: " << mk_pp(fml, m) << "\n";
ENSURE(m.is_true(fml));
// Issue #7403: mod (a + b) b should simplify to mod a b for symbolic b
// i.e. (= (mod (+ I S) S) (mod I S)) should reduce to true
fml = parse_int_fml(m, "(= (mod (+ I S) S) (mod I S))");
rw(fml);
std::cout << "mod (a+b) b = mod a b: " << mk_pp(fml, m) << "\n";
ENSURE(m.is_true(fml));
// mod (a + 2*b) b should simplify to mod a b (multiple of modulus dropped)
fml = parse_int_fml(m, "(= (mod (+ I (* 2 S)) S) (mod I S))");
rw(fml);
std::cout << "mod (a+2b) b = mod a b: " << mk_pp(fml, m) << "\n";
ENSURE(m.is_true(fml));
// mod (mod a b) b should simplify for non-zero numeral b
fml = parse_int_fml(m, "(= (mod (mod I 3) 3) (mod I 3))");
rw(fml);
std::cout << "mod (mod a 3) 3 = mod a 3: " << mk_pp(fml, m) << "\n";
ENSURE(m.is_true(fml));
}