mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-15 08:44:10 +00:00
Code Activity

Fix scaled_min test failure from #9235 mod-factor-propagation

Browse source 
The is_mod handler in theory_lra called ensure_nla(), which
unnecessarily created the NLA solver for pure linear problems, causing
the optimizer to return a finite value instead of -infinity.

Fix: check `m_nla` instead of calling `ensure_nla()`, matching the
pattern used by the is_idiv handler. The mod division is only registered
when NLA is already active due to nonlinear terms.

Update mod_factor tests to use QF_NIA logic and assert the mul term
before the mod term so that internalize_mul triggers ensure_nla() before
mod internalization.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This commit is contained in:
Arie Gurfinkel 2026-04-09 20:23:03 -04:00
parent 23ae00a57e
commit 956fa85c1b
2 changed files with 8 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_lra.cpp
View file

@ -472,8 +472,7 @@ class theory_lra::imp {
else if (a.is_mod(n, n1, n2)) {
if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n);
if (!ctx().relevancy()) mk_idiv_mod_axioms(n1, n2);
if (a.is_numeral(n2) && !r.is_zero()) {
ensure_nla();
if (m_nla && a.is_numeral(n2) && !r.is_zero()) {
app_ref div(a.mk_idiv(n1, n2), m);
ctx().internalize(div, false);
internalize_term(to_app(div));

13
src/test/mod_factor.cpp
View file

@ -10,17 +10,18 @@ Copyright (c) 2025 Microsoft Corporation
static void test_mod_factor_mod_path() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver s = Z3_mk_solver_for_logic(ctx, Z3_mk_string_symbol(ctx, "QF_NIA"));
Z3_solver_inc_ref(ctx, s);
Z3_sort int_sort = Z3_mk_int_sort(ctx);
Z3_ast x = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x"), int_sort);
Z3_ast y = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "y"), int_sort);
Z3_ast seven = Z3_mk_int(ctx, 7, int_sort);
Z3_ast zero = Z3_mk_int(ctx, 0, int_sort);
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, Z3_mk_mod(ctx, x, seven), zero));
Z3_ast xy_args[] = {x, y};
Z3_ast xy = Z3_mk_mul(ctx, 2, xy_args);
// assert mul term first so ensure_nla() fires before mod internalization
Z3_solver_assert(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, Z3_mk_mod(ctx, xy, seven), zero)));
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, Z3_mk_mod(ctx, x, seven), zero));
ENSURE(Z3_solver_check(ctx, s) == Z3_L_FALSE);
Z3_solver_dec_ref(ctx, s);
Z3_del_config(cfg);
@ -33,7 +34,7 @@ static void test_mod_factor_mod_path() {
static void test_mod_factor_idiv_path() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver s = Z3_mk_solver_for_logic(ctx, Z3_mk_string_symbol(ctx, "QF_NIA"));
Z3_solver_inc_ref(ctx, s);
Z3_sort int_sort = Z3_mk_int_sort(ctx);
Z3_ast x = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x"), int_sort);
@ -43,9 +44,7 @@ static void test_mod_factor_idiv_path() {
Z3_ast hundred = Z3_mk_int(ctx, 100, int_sort);
// xm = x mod 100 (bounded by is_bounded)
Z3_ast xm = Z3_mk_mod(ctx, x, hundred);
// xm mod 7 = 0
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, Z3_mk_mod(ctx, xm, seven), zero));
// (xm * y) div 7 — triggers idiv internalization with bounded dividend
// (xm * y) — assert mul term first so ensure_nla() fires before mod internalization
Z3_ast xm_y_args[] = {xm, y};
Z3_ast xm_y = Z3_mk_mul(ctx, 2, xm_y_args);
Z3_ast xm_y_div = Z3_mk_div(ctx, xm_y, seven);
@ -53,6 +52,8 @@ static void test_mod_factor_idiv_path() {
Z3_solver_assert(ctx, s, Z3_mk_not(ctx, Z3_mk_eq(ctx, Z3_mk_mod(ctx, xm_y, seven), zero)));
// use div to keep it alive
Z3_solver_assert(ctx, s, Z3_mk_ge(ctx, xm_y_div, zero));
// xm mod 7 = 0
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, Z3_mk_mod(ctx, xm, seven), zero));
ENSURE(Z3_solver_check(ctx, s) == Z3_L_FALSE);
Z3_solver_dec_ref(ctx, s);
Z3_del_config(cfg);