Incorrect model in mixed FP/Real logic triggered by extra string constraint

[wingsyuyi-satori]

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

[github-actions]

This issue appears closely related to #8194. Both involve incorrect models when :produce-proofs true is enabled, with correct behavior when disabled. The common pattern suggests a systematic problem in model reconstruction during proof generation, particularly when string theory constraints are present.

This comment was added by the automated Issue Backlog Processor.

Generated by Issue Backlog Processor

[github-actions]

This appears to be related to #8194 which also reports incorrect models when produce-proofs is enabled with String theory. Both issues suggest that proof generation mode is interfering with the correctness of the String theory solver.

As a workaround, removing :produce-proofs true allows Z3 to generate valid models.

Linking these issues for tracking purposes.

This comment was added by the automated Issue Backlog Processor.

Generated by Issue Backlog Processor

[wintered]

84a7566

$ z3 model_validate=true bug1.smt2
sat
(error "line 3 column 22: an invalid model was generated")
$ cat bug1.smt2
(declare-fun a () Real)
(assert (< 1.9 (/ 1.9 0.0)))
(check-sat-using qflia)