From a3c7dc94338ecfe4856ba22817d07ba6e4b0b9b5 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Thu, 23 Jul 2026 12:34:46 -0700 Subject: [PATCH] fix: smtlib2_compliant mode turns unsat to unknown due to Int/Real sort mismatch in coeffs2app (#10204) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit With `(set-option :smtlib2_compliant true)`, Z3 disables implicit Int→Real coercions. When the LP solver generates Gomory cuts/bounds over expressions that mix Int and Real LP variables (as happens when `to_real(n)` is internalized — both `to_real(n)` as Real and `n` as Int are registered as LP vars), `coeffs2app` was constructing `mk_mul(Real_numeral, Int_expr)`. Without implicit coercions, `check_args` throws an `ast_exception` that bubbles up through `cmd_context::check_sat()` as `l_undef`, producing a spurious `unknown` instead of `unsat`. ## Changes - **`src/smt/theory_lra.cpp` — `coeffs2app`**: Before building each product term, coerce `o` to Real via `a.mk_to_real(o)` when `!is_int && a.is_int(o)`. This makes the sort explicit rather than relying on implicit coercions. - **`src/test/smt2print_parse.cpp`**: Regression test for the exact formula from the issue — verifies the result is `unsat` (not `unknown`) when `smtlib2_compliant` is set. ```smt2 (set-option :smtlib2_compliant true) (set-logic ALL) (declare-datatype SBVRational ((SBV.Rational (sbv.rat.numerator Int) (sbv.rat.denominator Int)))) ; ... mixed Int/Real via to_real ... (check-sat) ; was: unknown (:reason-unknown "Sort mismatch at argument #2 for function * (Real Real) Real supplied sort is Int") ; now: unsat ``` - Fixes #10166 --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- src/smt/theory_lra.cpp | 5 ++++ src/test/smt2print_parse.cpp | 47 ++++++++++++++++++++++++++++++++++++ 2 files changed, 52 insertions(+) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 0248fe2dd0..9c4588f32a 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -4277,6 +4277,11 @@ public: expr_ref_vector args(m); for (auto const& [w, coeff] : coeffs) { expr* o = get_expr(w); + // When the overall expression is Real but 'o' is Int (e.g. due to + // to_real(Int) equality constraints in the LP), coerce 'o' to Real + // to avoid sort mismatches when int/real coercions are disabled. + if (!is_int && a.is_int(o)) + o = a.mk_to_real(o); if (coeff.is_zero()) { // continue } diff --git a/src/test/smt2print_parse.cpp b/src/test/smt2print_parse.cpp index 83920cabd8..f696a8349e 100644 --- a/src/test/smt2print_parse.cpp +++ b/src/test/smt2print_parse.cpp @@ -327,4 +327,51 @@ void tst_smt2print_parse() { test_symbol_escape(); + // Regression test for GitHub issue #10166: + // With (set-option :smtlib2_compliant true), a formula involving to_real + // and mixed Int/Real arithmetic should return "unsat", not "unknown". + { + char const* spec = + "(set-option :smtlib2_compliant true)\n" + "(set-logic ALL)\n" + "(declare-datatype SBVRational ((SBV.Rational (sbv.rat.numerator Int) (sbv.rat.denominator Int))))\n" + "(define-fun sbv.rat.eq ((x SBVRational) (y SBVRational)) Bool\n" + " (= (* (sbv.rat.numerator x) (sbv.rat.denominator y))\n" + " (* (sbv.rat.denominator x) (sbv.rat.numerator y))))\n" + "(define-fun s4 () Real 0.0)\n" + "(declare-fun s0 () SBVRational)\n" + "(assert (< 0 (sbv.rat.denominator s0)))\n" + "(declare-fun s1 () SBVRational)\n" + "(assert (< 0 (sbv.rat.denominator s1)))\n" + "(define-fun s2 () Int (sbv.rat.denominator s1))\n" + "(define-fun s3 () Real (to_real s2))\n" + "(define-fun s5 () Bool (= s3 s4))\n" + "(define-fun s6 () Int (sbv.rat.numerator s1))\n" + "(define-fun s7 () Real (to_real s6))\n" + "(define-fun s8 () Real (/ s7 s3))\n" + "(define-fun s9 () Real (ite s5 s4 s8))\n" + "(define-fun s10 () Int (sbv.rat.denominator s0))\n" + "(define-fun s11 () Real (to_real s10))\n" + "(define-fun s12 () Bool (= s4 s11))\n" + "(define-fun s13 () Int (sbv.rat.numerator s0))\n" + "(define-fun s14 () Real (to_real s13))\n" + "(define-fun s15 () Real (/ s14 s11))\n" + "(define-fun s16 () Real (ite s12 s4 s15))\n" + "(define-fun s17 () Bool (= s9 s16))\n" + "(define-fun s18 () Bool (sbv.rat.eq s0 s1))\n" + "(assert s17)\n" + "(assert (not s18))\n" + "(check-sat)\n"; + + Z3_context ctx = Z3_mk_context(nullptr); + Z3_set_error_handler(ctx, setError); + is_error = false; + std::string resp = Z3_eval_smtlib2_string(ctx, spec); + Z3_del_context(ctx); + std::cout << "Issue #10166 response: " << resp << "\n"; + ENSURE(!is_error); + ENSURE(resp.find("unsat") != std::string::npos); + ENSURE(resp.find("unknown") == std::string::npos); + } + }