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
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:
Output:
If I remove
(set-option :produce-proofs true)and run:Commit: 888d2fc