search

z3str / Z3-str

A Z3-Based String Constraint Solver
Other
87 stars 13 forks source link

Unsound result #2

Closed SaswatPadhi closed 9 years ago

SaswatPadhi commented 9 years ago

On the latest version, the following input:

(declare-const r String)
(declare-const s String)

(assert (= s "aa"))
(assert (= r (Concat (Replace s "aa" "x") "a")))

(assert (not (= (Length s) (Length r))))

(check-sat)

produces:

>> SAT
------------------------
s : string -> "aa"
r : string -> "aaa"
z3str commented 9 years ago

Hi Saswat,

Thanks for the feedback! This is a bug and it has been fixed. I just checked in the changes. Could you sync and try again?

Thanks, -Yunhui

SaswatPadhi commented 9 years ago

Awesome. It works as expected now.

Thanks Yunhui.