improved subset checking for regexes with counters

[veanes]

Two main edits.

1. Some cases with counters caused divergence of unsat checking.
   A common case is a regex with nested counting (a{0,k})*. where one gets
   disjuncts of the form a{0,k-1}(a{0,k})* | a{0,k-2}(a{0,k})* but where the first one subsumes the second one.
   The PR extends the is_subset check to avoid the blowup (in some cases).
   The problem is in general very hard though.

2. The PR also fixes an issue with Antimitov form that allowed unions of conditionals with the same condition,
   by simplifying them, essentally by turning if(c, t1, e1) U if(c, t2, e2) into if(c, t1 U t2, e1 U e2)

A related test I intend to add to the regression tests is this (that would before the fix not terminate):
I'll also add a few variants of it for unicode as well as ascii encodings.

(declare-const s String)
(assert (str.in_re s (re.inter (re.+ ((_ re.loop 1 100000) (str.to_re "a"))) (re.comp (re.++ re.all (str.to_re "a"))))))
(check-sat)