(z3str3) Soundness bug on QF_S formula with re.comp str.to_re

[muchang]

Hi,
For this case, Z3 gives an incorrect answer:

[573] % z3 smt.string_solver=z3str3 small.smt2 
sat
[574] % z3 small.smt2 
unsat
[575] % 
[575] % cat small.smt2 
(set-logic QF_S)
(assert (= (re.comp (str.to_re "")) (str.to_re "")))
(check-sat)
[576] %

OS: Ubuntu 18.04
Commit: f2d3160

[mtrberzi]

It occurs to me that I have never thought about the semantics of asserting that two RegLan terms are equal or unequal before. Is this meaningful according to the SMT-LIB standard? I wonder what is expected here. theory_seq says that this is UNSAT. What is that based on, is it a syntactic check or are the semantics of the terms here actually considered? Either way I think support for this can be added relatively quickly once I understand what the solver has to do with this kind of equality.

[NikolajBjorner]

Checking equality of regular languages S, R reduces to checking emptiness of R \ S and S \ R.
Checking emptiness/non-emptiness (difference of regular languages) is handled in seq_regex.cpp using a custom procedure that unfolds a regular expression.
Checking emptiness of regular languages without complementation or intersection and without symbolic sub-expressions can be accomplished with linear overhead. The rewriter simplifier probably already contains some shortcuts for this.