From b402268d3532debf140253190b39b4dce4eaf9d0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 29 Jan 2021 06:43:33 -0800
Subject: [PATCH] fix #4982

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_rewriter.cpp |  6 ++++++
 src/smt/seq_eq_solver.cpp         | 14 ++++++++++++++
 src/smt/theory_seq.h              |  1 +
 3 files changed, 21 insertions(+)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index ebfb7e14c..e7bb70da6 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -1383,6 +1383,12 @@ br_status seq_rewriter::mk_seq_nth_i(expr* a, expr* b, expr_ref& result) {
     }
     unsigned len = r.get_unsigned();
 
+    expr* a2, *i2;
+    if (len == 0 && str().is_at(a, a2, i2) && m_autil.is_numeral(i2, r) && r.is_zero()) {
+        result = str().mk_nth_i(a2, i2);
+        return BR_REWRITE1;
+    }
+
     expr_ref_vector as(m());
     str().get_concat_units(a, as);
 
diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp
index e8b983e09..351ec1ed4 100644
--- a/src/smt/seq_eq_solver.cpp
+++ b/src/smt/seq_eq_solver.cpp
@@ -1577,6 +1577,16 @@ bool theory_seq::is_ternary_eq_lhs(expr_ref_vector const& ls, expr_ref_vector co
     return false;
 }
 
+struct remove_obj_pair_map : public trail<context> {
+    obj_pair_hashtable<expr, expr> & m_map;
+    expr* a, *b;
+    remove_obj_pair_map(obj_pair_hashtable<expr, expr> & map, expr* a, expr* b):
+        m_map(map), a(a), b(b) {}
+    void undo(context& ctx) override {
+        m_map.erase(std::make_pair(a, b));
+    }
+};
+
 /**
    nth(x,idx) = rhs => 
    x = pre(x, idx) ++ unit(rhs) ++ post(x, idx + 1)
@@ -1591,6 +1601,10 @@ bool theory_seq::solve_nth_eq2(expr_ref_vector const& ls, expr_ref_vector const&
         expr_ref idx1(m_autil.mk_add(idx, m_autil.mk_int(1)), m);
         m_rewrite(idx1);
         expr_ref rhs = mk_concat(rs.size(), rs.c_ptr(), m.get_sort(ls[0]));
+        if (m_nth_eq2_cache.contains(std::make_pair(rhs, ls[0])))
+            return false;
+        m_nth_eq2_cache.insert(std::make_pair(rhs, ls[0]));
+        ctx.push_trail(remove_obj_pair_map(m_nth_eq2_cache, rhs, ls[0]));
         ls1.push_back(s);        
         if (!idx_is_zero) rs1.push_back(m_sk.mk_pre(s, idx)); 
         rs1.push_back(m_util.str.mk_unit(rhs)); 
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 71a728a38..58b5bda1f 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -459,6 +459,7 @@ namespace smt {
         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_eq1(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
+        obj_pair_hashtable<expr, expr> m_nth_eq2_cache;
         bool solve_nth_eq2(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
         bool solve_itos(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
         bool solve_itos(expr* n, expr_ref_vector const& rs, dependency* dep);