search

z3str / Z3-str

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

Unknown result when concatenating twice the same variable #16

Open jad-hamza opened 7 years ago

jad-hamza commented 7 years ago

The following formula produces UNKNOWN (1) using the latest github code

(set-option :auto-config true)
(set-option :produce-models true)

(declare-variable a String)
(declare-variable b String)

(assert (= (Concat a a) b))

(check-sat)
(get-model)