Hiroshi Unno

icon indicating a website link https://www.riec.tohoku.ac.jp/~unno/ icon indicating an email [email protected]

icon company Tohoku University

Results 1 issues of Hiroshi Unno

A simple regex constraint for which dZ3 returns unknown

Hi, For the following simple instance, z3 (https://github.com/Z3Prover/z3/commit/f7d9a5ba935163ddefd3e1883878556d713d6fee) without enabling z3str3 immediately returns unknown. ``` $ cat dz3_unknown.smt2 (assert (or (= re.all (re.union (str.to_re "y") (re.comp (str.to_re "x")))) (= re.all...