search

z3str / Z3-str

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

UNKNOWN output for combination of startsWith and Regex #8

Open yannicnoller opened 8 years ago

yannicnoller commented 8 years ago

Hey all,

I tried the following input:

(declare-variable x String)
(assert (= (Length x) 2))
(assert (RegexIn x (RegexStar (RegexCharRange "a" "z"))))
(assert (StartsWith x "a"))
(check-sat)
(get-model)

and I get the following result:

* v-fail
************************
>> UNKNOWN  (1)
************************
>> etime(s) = 0.178010

Why is it not possible to solve this constraint with z3-str? Or am I doing something wrong?

Cheers, Yannic

z3str commented 8 years ago

Thanks! I will look into it and keep you posted.

sduchovn-akam commented 8 years ago

I'm also getting this error message; the input

(declare-variable x String)
(declare-variable y String)

(assert (= "/" (CharAt x 0)))
(assert (= x (Concat y "/")))

(check-sat)
(get-model)

produces

* v-fail
************************
>> UNKNOWN  (1)
************************
>> etime(s) = 0.055382

The raw output of str is

************************
>> SAT
------------------------
$$_xor_0 : int -> 0
$$_str2 : string -> String!val!0
$$_str0 : string -> ""
y : string -> String!val!2
x : string -> String!val!1
$$_str1 : string -> "/"
$$_str3 : string -> String!val!2
************************

Any idea what might be causing this? I've attached the log file produced by str.

z3-str-log.txt