search

z3str / Z3-str

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

echo function does not work #13

Open aalhuz opened 8 years ago

aalhuz commented 8 years ago

Hi I was testing the following code

(declare-variable X String) (declare-variable Y1 String) (declare-variable Y2 String) (declare-variable Z String) (declare-variable M String)

(echo "before reset") (assert (= Z (Concat X "gkhi" ) ) ) (assert (= Z (Concat Y1 Y2 ) ) ) (assert (= Z (Concat "abcd" M ) ) )

(check-sat) (get-model)

And I got this error after adding a call to 'echo' (error .. invalid command argument, string expected") Does this mean that this function is not supported in Z3-str?

Thanks

Shirlies commented 8 years ago

Hi Did you use the binary file which compilered from C++ code with the input?

Kind Regards Shirlies