Rewriting string rewriter

[jurajsic]

The current rewriter of Z3 does a lot of unknown stuff for us, and some of it can be damaging for noodler. Sometimes it even brings stuff from seq theory, for example by running this

(set-logic QF_S)
(declare-fun s1 () String)
(assert (str.in_re "abbbe" (str.to_re s1)))
(check-sat)

we get (seq.nth_i s1 0) in relevant_eh() which we cannot handle right now.

[vhavlena]

Interesting. On the other hand, the constraint you gave contains variable inside a regex, which is currently out of our scope.