Investigate invalid model in mixed FP/Real logic triggered by string constraint with produce-proofs

[Copilot]

Z3 returns sat with a model-validation failure when produce-proofs=true is combined with mixed FP/Real/Int logic and a string constraint like (assert (and x (= (str.from_int 0) "0"))). Removing either the string constraint or produce-proofs causes Z3 to return unknown instead.

Root Cause (Investigation)

• Simplification silently removes string terms: mk_simplify_tactic (run first in default_tactic before probe evaluation) folds (str.from_int 0) → "0", making (= "0" "0") → true and dropping all string ops from the goal. Probes then see a formula with no strings.
• Theory combination gap under proofs: The integer variable x8 bridges both the BV/FP world (via (to_fp 8 24 RNE (to_real x8))) and the arith world (via (ite ... x8 1)). With produce-proofs=true, the BV model assigned to x8 by theory_fpa can diverge from the arith model, yielding an internally inconsistent model — e.g. x8=0, s(x)=0.0 violating (+ (s 0.0) (ite fp-condition x8 1)) > 0.

Status

This PR captures the investigation. The current codebase exhibits a related regression: both with and without the string constraint the solver runs indefinitely rather than returning unknown. A targeted fix to enforce model consistency between the FP/BV and arithmetic theory models, or to conservatively block qffplra selection when Int variables appear in FP coercions, is needed.

Original prompt

---

This section details on the original issue you should resolve

<issue_title>Incorrect model in mixed FP/Real logic triggered by extra string constraint</issue_title>
<issue_description>Z3 reports sat but generates an invalid model (fails model_validate=true).

Crucially, this behavior is triggered by the inclusion of a seemingly irrelevant String constraint: (assert (and x (= (str.from_int 0) "0"))). If I remove this constraint or remove (set-option :produce-proofs true), Z3 returns unknown instead of producing the incorrect model.

Input:

(set-option :produce-proofs true)
(declare-const x8 Int)
(declare-const x Bool)
(declare-fun s (Real) Real)
(assert (> 
    (+ (s 0.0) 
        (ite (fp.isNormal 
            (fp.fma RNE 
                (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)) 
                ((_ to_fp 8 24) RNE (to_real x8)) 
                ((_ to_fp 8 24) RNE 0.5)))
            x8 
            1)) 
    0.0)
)
(assert (and x (= (str.from_int 0) "0")))
(check-sat)
(get-model)

Output:

z3 test.smt2 model_validate=true
sat
(error "line 17 column 10: an invalid model was generated")
(
  (define-fun x () Bool
    true)
  (define-fun x8 () Int
    0)
  (define-fun /0 ((x!0 Real) (x!1 Real)) Real
    (/ 1.0 126.0))
  (define-fun s ((x!0 Real)) Real
    0.0)
)

For reference, cvc5 solves this instance correctly and produces a valid model.

sat
(
(define-fun x8 () Int (- 2))
(define-fun x () Bool true)
(define-fun s ((_arg_1 Real)) Real 3.0)
)

Commit: eca8e19</issue_description>

Comments on the Issue (you are @copilot in this section)

• Fixes Incorrect model in mixed FP/Real logic triggered by extra string constraint #8185

---

💡 You can make Copilot smarter by setting up custom instructions, customizing its development environment and configuring Model Context Protocol (MCP) servers. Learn more Copilot coding agent tips in the docs.