search

VeriFIT / z3-noodler

The Z3-Noodler String Solver
Other
9 stars 5 forks source link

Bug for not contains #157

Closed jurajsic closed 3 months ago

jurajsic commented 4 months ago

Current devele returns sat for

(set-logic QF_S)
(set-info :status unsat)
(declare-const a String)
(declare-const b String)
(assert (= a b))
(assert (str.contains "abc" a ))
(assert (not (str.contains "abcde" b )))
(check-sat)
(exit)

even though it should be unsat.

I think this will be fixed in #150, right?

vhavlena commented 4 months ago

Yes, I got unsat in the ca-diseqs branch.

vhavlena commented 3 months ago

I am closing the issue as it was solved by #150