Investigate: Invalid model with :produce-proofs true in String Theory + UF

[Copilot]

Z3 reports sat with a model that fails validation when :produce-proofs true is set alongside String Theory and uninterpreted functions. Removing :produce-proofs true produces a valid model.

Root Cause (Investigation Only — No Fix Implemented Yet)

This PR documents findings from root cause analysis. No code changes were made.

What happens with proofs enabled

• propagate_values() and flatten_clauses() in asserted_formulas.cpp are skipped when m.proofs_enabled(), causing the solver to explore different search branches
• The solver selects e="A", x=0, making str.substr("A",0,1) = "A" = e, so the ITE branch evaluates to the same string as e

Why the contradiction is missed

• internalize_ite_term() in smt_internalizer.cpp returns early (line 832–834) without calling apply_sort_cnstr(), so the ITE enode never gets a theory variable in theory_seq
• Without a theory variable, check_extensionality() in theory_seq.cpp never compares the ITE root against e, failing to call ctx.assume_eq() that would surface the UF contradiction (n(ite,"@")=1 vs n(e,"@")=0)

Model generation artifact

mk_func_interps() then produces two conflicting entries for the same function n:

["A", "@"] → 0   (from n(e, "@"))
["A", "@"] → 1   (from n(ite, "@"))  ← silently dropped

The first entry wins, yielding n("A","@") = 0, which violates assertion 3.

Proposed Fix Direction

Ensure the ITE term receives a theory_seq theory variable (by calling apply_sort_cnstr for ITE terms of sequence sort), so check_extensionality considers it and triggers the necessary assume_eq to expose the UF contradiction before the solver declares SAT.

Original prompt

---

This section details on the original issue you should resolve

<issue_title>Incorrect model with :produce-proofs true involving String Theory and UF</issue_title>
<issue_description>Z3 reports sat but generates an invalid model.

The issue seems strictly related to proof generation. If I remove (set-option :produce-proofs true), Z3 successfully produces a valid model.

Input:

(set-logic ALL)
(set-option :produce-proofs true)
(declare-const x Int)
(declare-fun n (String String) Int)
(declare-const e String)
(declare-const d String)
(assert (= d (str.++ e "@")))
(assert (= 0 (n e "@")))
(assert (= 1 (n (ite (= 0 (str.len (str.substr d 0 1))) "" (str.substr e x 1)) "@")))
(check-sat)
(get-model)

Output:

z3 model_validate=true test.smt2 
sat
(error "line 10 column 10: an invalid model was generated")
(
  (define-fun e () String
    "A")
  (define-fun x () Int
    0)
  (define-fun d () String
    "A@")
  (define-fun n ((x!0 String) (x!1 String)) Int
    0)
)

If I remove (set-option :produce-proofs true) and run:

sat
(
  (define-fun e () String
    "@")
  (define-fun x () Int
    2)
  (define-fun d () String
    "@@")
  (define-fun n ((x!0 String) (x!1 String)) Int
    (ite (and (= x!0 "") (= x!1 "@")) 1
      0))
)

Commit: 888d2fc</issue_description>

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

• Fixes Incorrect model with :produce-proofs true involving String Theory and UF #8194

---

💡 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.