From 956fa85c1b8fb51ab732cd0cf32ef89efc8c4dd8 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 9 Apr 2026 20:23:03 -0400 Subject: [PATCH] Fix scaled_min test failure from #9235 mod-factor-propagation 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) --- src/smt/theory_lra.cpp | 3 +-- src/test/mod_factor.cpp | 13 +++++++------ 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 1fc06b079..23c102874 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -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)); diff --git a/src/test/mod_factor.cpp b/src/test/mod_factor.cpp index 68aeab7dd..069802522 100644 --- a/src/test/mod_factor.cpp +++ b/src/test/mod_factor.cpp @@ -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);