Soundness bug in z3str3

[numairmansur]

Hi @mtrberzi

On the following file i get unsat with z3str3
qf_s.smt2

z3-seq correctly return sat

commit: e63992c

[mtrberzi]

Interesting -- I may have a fix for this in another branch, but taking a look.

[NikolajBjorner]

Two new refutation unsoundness instances for z3str3:

[527] % z3release test1.smt2 
sat
[528] % z3release test2.smt2 
sat
[529] % z3release smt.string_solver=z3str3 test1.smt2 
unsat
[530] % z3release smt.string_solver=z3str3 test2.smt2 
unsat
[531] % cat test1.smt2 
(declare-fun a () String)
(assert (not (str.in_re (str.++ "a" a) (re.inter (re.* (str.to_re "ab")) (re.* (str.to_re "a"))))))
(check-sat)
[532] % cat test2.smt2 
(declare-fun a () String)
(assert (not (and (str.in_re a (re.opt re.allchar)) (not (str.in_re a (re.opt re.allchar))))))
(check-sat)
[533] % 

OS: Ubuntu 18.04
Commit: ac39ddb

[mtrberzi]

Turns out these three issues are in fact related to the same piece of code in theory_str_regex.cpp (most likely). This is convenient since I'll hopefully be able to deal with all three of these bugs in one patch. There's a bit of theoretical hoop-jumping I need to do first as the logic here is a bit tricky, but the patch should be on the way soon.

[mtrberzi]

Opened #4595