Consolidate issues on string formulas

[rainoftime]

z3 40159a3

(set-option :smt.arith.bounded_expansion true)
(declare-fun v1 () Bool)
(declare-fun v2 () Bool)
(declare-fun v3 () Bool)
(declare-fun v6 () Bool)
(declare-fun v8 () Bool)
(declare-fun v13 () Bool)
(declare-fun i2 () Int)
(declare-fun i15 () Int)
(declare-fun str1 () String)
(declare-fun str2 () String)
(declare-fun str4 () String)
(declare-fun str6 () String)
(declare-fun str8 () String)
(declare-fun str11 () String)
(declare-fun str13 () String)
(declare-fun str15 () String)
(declare-fun str16 () String)
(push 1)
(check-sat)
(pop 1)
(assert (= true true true true (str.in_re str15 (str.to_re "")) true))
(declare-fun v16 () Bool)
(assert (or v1 true (str.in_re (str.substr str16 64 (abs (abs i2))) (str.to_re str13)) (str.in_re str4 (str.to_re "BffzmoGsWHteAoPbmbhWcbgP"))))
(push 1)
(pop 1)
(assert (= str1 str4))
(push 1)
(check-sat)
(pop 1)
(declare-fun v20 () Bool)
(assert (or v16 v13))
(push 1)
(check-sat)

sat
sat
ASSERTION VIOLATION
File: ../src/smt/theory_seq.cpp
Line: 3077
n1->get_root() != n2->get_root()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB