z3str3 invalid model on formula with str.indexof #3020
Description
Hi,
For this formula:
(declare-fun r () String)
(declare-fun s () String)
(declare-fun t () String)
(assert (= s t))
(assert (= (str.indexof s r 1) (str.indexof t r 0)))
(check-sat)
(get-model)
Z3 smt.string_solver=z3str3 gives an invalid model:
(model
(define-fun t () String
"?")
(define-fun r () String
"?")
(define-fun s () String
"?")
)
if I feed this model to the formula, Z3 reports unsat.
if we swap '0' with '1' from the bug-triggering test, z3str3 now gives a correct model:
[525] % z3 smt.string_solver=z3str3 model_validate=true small2.smt2
sat
(model
(define-fun t () String
"?")
(define-fun r () String
"\x00\x00")
(define-fun s () String
"?")
)
[526] % cat small2.smt2
(declare-fun r () String)
(declare-fun s () String)
(declare-fun t () String)
(assert (= s t))
(assert (= (str.indexof s r 0) (str.indexof t r 1)))
(check-sat)
(get-model)
OS: Ubuntu 18.04
Commit: aaf2c3b