fix build regression

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/rewriter/seq_rewriter.cpp

@@ -1584,45 +1584,12 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
     return BR_REWRITE3;
 }
 
-/**
- * t = (concat (unit (nth t 0)) (unit (nth t 1)) (unit (nth t 2)) .. (unit (nth t k-1)))
- * ->
- * (length t) = k
- */
-bool seq_rewriter::reduce_nth_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs) {
-    if (ls.size() == 1 && !rs.empty()) {
-        expr* l = ls.get(0);
-        for (unsigned i = 0; i < rs.size(); ++i) {
-            unsigned k = 0;
-            expr* ru = nullptr, *r = nullptr;
-            if (m_util.str.is_unit(rs.get(i), ru) && m_util.str.is_nth(ru, r, k) && k == i && r == l) {
-                continue;
-            }
-            return false;
-        }
-        arith_util a(m());
-        lhs.push_back(m_util.str.mk_length(l));
-        rhs.push_back(a.mk_int(rs.size()));
-        ls.reset();
-        rs.reset();
-        return true;
-    }
-    else if (rs.size() == 1 && !ls.empty()) {
-        return reduce_nth_eq(rs, ls, rhs, lhs);
-    }
-    return false;
-}
-
 bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change) {
     expr* a, *b;
     zstring s;
     bool lchange = false;
     SASSERT(lhs.empty());
     TRACE("seq", tout << ls << "\n"; tout << rs << "\n";);
-    if (reduce_nth_eq(ls, rs, lhs, rhs)) {
-        change = true;
-        return true;
-    }
     // solve from back
     while (true) {
         while (!rs.empty() && m_util.str.is_empty(rs.back())) {

src/ast/rewriter/seq_rewriter.h

@@ -170,8 +170,6 @@ public:
 
     bool reduce_contains(expr* a, expr* b, expr_ref_vector& disj);
 
-    bool reduce_nth_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs);
-
     void add_seqs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_vector& lhs, expr_ref_vector& rhs);
 
 

src/smt/theory_seq.cpp

@@ -2292,6 +2292,26 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
     return true;
 }
 
+bool theory_seq::solve_nth_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependency* deps) {
+    if (ls.size() != 1) return false;
+    expr_ref l(ls.get(0), m);
+    for (unsigned i = 0; i < rs.size(); ++i) {
+        unsigned k = 0;
+        expr* ru = nullptr, *r = nullptr;
+        if (m_util.str.is_unit(rs.get(i), ru) && m_util.str.is_nth(ru, r, k) && k == i && r == l) {
+            continue;
+        }
+        return false;
+    }
+    add_solution(l, mk_concat(rs, m.get_sort(l)), deps);
+    expr_ref r(m_autil.mk_int(rs.size()), m);
+    ls.reset();
+    rs.reset();
+    ls.push_back(m_util.str.mk_length(l));
+    rs.push_back(r);
+    return true;
+}
+
 bool theory_seq::solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* deps) {
     if (l.size() == 1 && is_var(l[0]) && !occurs(l[0], r) && add_solution(l[0], mk_concat(r, m.get_sort(l[0])), deps)) {
         return true;
@@ -2446,6 +2466,12 @@ bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, de
         TRACE("seq", tout << "binary\n";);
         return true;
     }
+    if (!ctx.inconsistent() && solve_nth_eq(ls, rs, deps)) {
+        change = true;
+    }
+    if (!ctx.inconsistent() && solve_nth_eq(rs, ls, deps)) {
+        change = true;
+    }
     if (!ctx.inconsistent() && change) {
         // The propagation step from arithmetic state (e.g. length offset) to length constraints
         if (get_context().get_scope_level() == 0) {

src/smt/theory_seq.h

@@ -432,6 +432,7 @@ namespace smt {
         bool simplify_eq(expr_ref_vector& l, expr_ref_vector& r, dependency* dep);
         bool solve_unit_eq(expr* l, expr* r, dependency* dep);
         bool solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
+        bool solve_nth_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependency* dep);
         bool is_binary_eq(expr_ref_vector const& l, expr_ref_vector const& r, expr_ref& x, ptr_vector<expr>& xunits, ptr_vector<expr>& yunits, expr_ref& y);
         bool is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref& x1, expr_ref_vector& xs, expr_ref& x2, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2);
         bool is_ternary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref& x, expr_ref_vector& xs, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2, bool flag1);