search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

String theory inconsistency #2058

Closed varming closed 5 years ago

varming commented 5 years ago

The SMTLIB program:

(declare-const X String)
(declare-const Y String)

(assert (str.in.re X (re.++ (str.to.re "ref-") (str.to.re Y))))
(assert (str.in.re X (re.++ (str.to.re "ref-12") re.allchar (str.to.re "45"))))
(assert (str.in.re Y (re.++ re.allchar (str.to.re "2345"))))

(check-sat)
(get-model)

returns a model

(model 
  (define-fun Y () String
    "\x002345")
  (define-fun X () String
    "ref-12\x0045")
)

but the model does not satisfy the first assertion in the program.

I built z3 from b0fe7d9a219f60a66a31b07c3413105b09830988 and invoked it using:

./z3 -smt2 -T:24 smt.string_solver=seq ../incon.txt
NikolajBjorner commented 5 years ago

(str.to.re Y): regular expressions over variables isn't supported (the languages are no longer regular). Z3 should have thrown an error.