Solving with regular constraints doesn't finish in unsat case

[Lozov-Petr]

We are hacking formulas with a theory of regular languages. In two cases below first one reports unsat correctly, but second one hangs. It looks like combination of propositional language and regular constraints has missing optimization: the negation of str.in.re should be simplified to str.in.re (re.complement.... Is it a bug? Is our understanding correct?

CC @kakadu

(declare-const a String)

(set-info :status unsat)


(assert 
  (str.in.re a 
    (re.inter 
      (re.complement 
        (re.++
          (re.* (re.range "a" "z"))
          (re.union
            (str.to.re "string")
            (str.to.re "builder")
            (str.to.re "buffer")
          ))) 
      (re.++
        (re.* (re.range "a" "z"))
        (str.to.re "string")
        (re.opt
            (re.union
                (str.to.re "builder")
                (str.to.re "buffer")
      ))))))

(check-sat)
\

2nd

(declare-const a String)
(declare-const l1 Bool)
(declare-const l2 Bool)

(set-info :status unsat)

(assert (not (= l1
    (str.in.re a (re.++
        (re.* (re.range "a" "z"))
        (re.union
            (str.to.re "string")
            (str.to.re "builder")
            (str.to.re "buffer")
        ))))))
(assert (= l2
    (str.in.re a (re.++
        (re.* (re.range "a" "z"))
        (str.to.re "string")
        (re.opt
            (re.union
                (str.to.re "builder")
                (str.to.re "buffer")
            ))))))

(assert (and l1 l2))
(check-sat)