fix: smtlib2_compliant mode turns unsat to unknown due to Int/Real sort mismatch in coeffs2app (#10204)

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
```

<!-- START COPILOT CODING AGENT SUFFIX -->

- Fixes #10166

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>

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
             }

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);
+    }
+
 }