fix str.at rewrite

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Oct 7, 2019 · 9a516e5 · 9a516e5
1 parent a8e7074
commit 9a516e5
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 1 deletion.
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
@@ -1007,9 +1007,13 @@ br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) {
     unsigned i = 0;
     for (; i < m_lhs.size(); ++i) {
         expr* lhs = m_lhs.get(i);
-        if (lens.contains(lhs)) {
+        if (lens.contains(lhs) && !r.is_neg()) {
             lens.erase(lhs);
         }
+        else if (m_util.str.is_unit(lhs) && r.is_zero() && lens.empty()) {
+            result = lhs;
+            return BR_REWRITE1;
+        }
         else if (m_util.str.is_unit(lhs) && r.is_pos()) {
             r -= rational(1);
         }

diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
@@ -1586,6 +1586,9 @@ namespace nlsat {
                     check_lemma(c->size(), c->c_ptr(), false, nullptr);
                 }
             }
+            for (clause* c : m_learned) {
+                IF_VERBOSE(0, display(verbose_stream() << "KEEP: ", c->size(), c->c_ptr()) << "\n");
+            }
             assumptions.reset();
             assumptions.append(result);
             return r;