(z3str3, horn) Soundness bug on QF_S formula with str.replace_all

Z3Prover / z3

The Z3 Theorem Prover

Other

10.41k stars 1.47k forks source link

(z3str3, horn) Soundness bug on QF_S formula with str.replace_all #4408

Closed muchang closed 4 years ago

muchang commented 4 years ago

Hi, For this case, Z3 gives an incorrect answer:

[584] % z3 small.smt2
unknown
unknown
[585] % z3 smt.string_solver=z3str3 small.smt2
unsat
sat
[586] % 
[586] % cat small.smt2
(assert (= (str.replace_all "" "" "") ""))
(check-sat-using horn)
(check-sat)
[587] %

OS: Ubuntu 18.04 Commit: f2d3160

NikolajBjorner commented 4 years ago

most likely a duplicate: there are too many unsoundess bugs open at this time and debugging the case where "horn" tactics are invoked is too low priority.