Invalid model for String formula (z3str3)

Z3Prover / z3

The Z3 Theorem Prover

Other

10.41k stars 1.47k forks source link

Invalid model for String formula (z3str3) #4411

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula, z3 (commit 1dcbde4) gives an invalid model

(set-option :model_validate true)
(set-option :smt.string_solver z3str3)
(declare-const i5 Int)
(assert (>= (str.len (str.from_code i5)) 42))
(check-sat)

zhendongsu commented 4 years ago

Should be a dup of https://github.com/Z3Prover/z3/issues/4409