From 3a7df2c6ef6518c8fcae8b136b318023e50d8e7e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 3 Jun 2020 12:28:32 -0700
Subject: [PATCH] fix various nullability checks in seq_regex

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/transforms/dl_mk_array_blast.cpp |  1 -
 src/nlsat/nlsat_solver.cpp               |  4 +++-
 src/qe/qe_arith_plugin.cpp               | 11 ++++-------
 src/smt/seq_regex.cpp                    | 22 +++++++++++++++-------
 4 files changed, 22 insertions(+), 16 deletions(-)

diff --git a/src/muz/transforms/dl_mk_array_blast.cpp b/src/muz/transforms/dl_mk_array_blast.cpp
index a8093634d..e32ddf269 100644
--- a/src/muz/transforms/dl_mk_array_blast.cpp
+++ b/src/muz/transforms/dl_mk_array_blast.cpp
@@ -324,7 +324,6 @@ namespace datalog {
         }
         scoped_ptr<rule_set> rules = alloc(rule_set, m_ctx);
         rules->inherit_predicates(source);
-        rule_set::iterator it = source.begin(), end = source.end();
         bool change = false;
         for (rule* r : source) {
             if (m_ctx.canceled())
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index a7dbedca4..3e4773f7e 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -1967,7 +1967,9 @@ namespace nlsat {
         bool resolve(clause const & conflict) {
             clause const * conflict_clause = &conflict;
             m_lemma_assumptions = nullptr;
-        start:
+			std::cout << "resolve\n";
+		start:
+			std::cout << "start\n";
             SASSERT(check_marks());
             TRACE("nlsat_proof", tout << "STARTING RESOLUTION\n";);
             TRACE("nlsat_proof_sk", tout << "STARTING RESOLUTION\n";);
diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp
index 6b7eb2897..30b09a381 100644
--- a/src/qe/qe_arith_plugin.cpp
+++ b/src/qe/qe_arith_plugin.cpp
@@ -2412,24 +2412,21 @@ public:
         }
 
         bool update_bounds(contains_app& contains_x, expr* fml) {
-            bounds_proc* bounds = nullptr;
-            if (m_bounds_cache.find(contains_x.x(), fml, bounds)) {
+            bounds_proc* _bounds = nullptr;
+            if (m_bounds_cache.find(contains_x.x(), fml, _bounds)) {
                 return true;
             }
-            bounds = alloc(bounds_proc, m_util);
-
+            scoped_ptr<bounds_proc> bounds = alloc(bounds_proc, m_util);
             if (!update_bounds(*bounds, contains_x, fml, m_ctx.pos_atoms(), true)) {
-                dealloc(bounds);
                 return false;
             }
             if (!update_bounds(*bounds, contains_x, fml, m_ctx.neg_atoms(), false)) {
-                dealloc(bounds);
                 return false;
             }
             
             m_trail.push_back(contains_x.x());
             m_trail.push_back(fml);
-            m_bounds_cache.insert(contains_x.x(), fml, bounds);
+            m_bounds_cache.insert(contains_x.x(), fml, bounds.detach());
             return true;
         }
     };
diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp
index 30d7b66c3..4ca6cdbf7 100644
--- a/src/smt/seq_regex.cpp
+++ b/src/smt/seq_regex.cpp
@@ -195,11 +195,22 @@ namespace smt {
         VERIFY(sk().is_accept(e, s, i, idx, r));
         expr_ref is_nullable(m), d(r, m);
 
+
         TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";);
 
         if (block_unfolding(lit, idx))
             return true;
 
+        literal_vector conds;
+        conds.push_back(~lit);
+        if (!unfold_cofactors(d, conds)) 
+            return false;
+
+        if (re().is_empty(d)) {
+            th.add_axiom(conds);
+            return true;
+        }
+
         // s in R & len(s) <= i => nullable(R)
         literal len_s_le_i = th.m_ax.mk_le(th.mk_len(s), idx);
         switch (ctx.get_assignment(len_s_le_i)) {
@@ -207,25 +218,22 @@ namespace smt {
             ctx.mark_as_relevant(len_s_le_i);
             return false;
         case l_true: 
-            is_nullable = seq_rw().is_nullable(r);
+            is_nullable = seq_rw().is_nullable(d);
             rewrite(is_nullable);
-            th.add_axiom(~lit, ~len_s_le_i, th.mk_literal(is_nullable));
+            conds.push_back(~len_s_le_i);
+            conds.push_back(th.mk_literal(is_nullable));            
+            th.add_axiom(conds);
             return true;
         case l_false:
             break;
         }
 
-        literal_vector conds;
-        if (!unfold_cofactors(d, conds)) 
-            return false;
-
         // (accept s i R) & len(s) > i => (accept s (+ i 1) D(nth(s, i), R)) or conds
         expr_ref head = th.mk_nth(s, i);
         d = re().mk_derivative(head, r);
         rewrite(d);
 
         literal acc_next = th.mk_literal(sk().mk_accept(s, a().mk_int(idx + 1), d));
-        conds.push_back(~lit);
         conds.push_back(len_s_le_i);
         conds.push_back(acc_next);
         th.add_axiom(conds);