search

uuverifiers / ostrich

An SMT Solver for string constraints
Other
35 stars 8 forks source link

QF_S solution soundness bug with str.at #29

Closed muchang closed 3 years ago

muchang commented 3 years ago 
[523] % z3release small.smt2
unsat
[524] % cvc4 -q --strings-exp small.smt2
unsat
[525] % ostrich +quiet small.smt2
sat
[526] % 
[526] % cat small.smt2
(declare-fun a () String)
(assert (not (= (str.at a 0) (str.at "" 0))))
(assert (= (str.len a) 0))
(check-sat)
[527] %

Or

[612] % z3release small.smt2
unsat
[613] % cvc4 -q --strings-exp small.smt2
unsat
[614] % ostrich +quiet small.smt2
sat
[615] % 
[615] % cat small.smt2 
(declare-fun x () String)
(assert (distinct (str.at (str.++ "A" x) 1) (str.at x 0)))
(check-sat)
[616] %

Commit: 2f3ea5c

pruemmer commented 3 years ago

Thanks for the bug report! Those inputs are not actually in the fragment supported by OSTRICH, they are not straightline formulas. The latest master includes stricter checks for this.

The first problem can also be handled correctly now, but in general negated equations between string variables are not (yet) supported.

muchang commented 3 years ago

Thanks for your fix! This issue can be closed now.