From 9fa17a432a51cd864d543b041e6985e8a028dcfb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 13 Nov 2020 17:05:10 -0800
Subject: [PATCH] bug fixes in nullability check

@veanes @cdstanford
---
 src/ast/rewriter/seq_rewriter.cpp | 8 ++++----
 src/smt/seq_regex.cpp             | 1 +
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 666736cfa..e66daa845 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -2302,17 +2302,17 @@ expr_ref seq_rewriter::is_nullable_rec(expr* r) {
 
 expr_ref seq_rewriter::is_nullable_symbolic_regex(expr* r, sort* seq_sort) {
     SASSERT(m_util.is_re(r));
-    expr* elem = nullptr, * r2 = nullptr, * s = nullptr;
+    expr* elem = nullptr, *r1 = r, * r2 = nullptr, * s = nullptr;
     expr_ref elems(str().mk_empty(seq_sort), m());
     expr_ref result(m());
-    while (re().is_derivative(r, elem, r2)) {
+    while (re().is_derivative(r1, elem, r2)) {
         if (str().is_empty(elems))
             elems = str().mk_unit(elem);
         else
             elems = str().mk_concat(str().mk_unit(elem), elems);
-        r = r2;
+        r1 = r2;
     }
-    if (re().is_to_re(r, s)) {
+    if (re().is_to_re(r1, s)) {
         // r is nullable  
         // iff after taking the derivatives the remaining sequence is empty 
         // iff the inner sequence equals to the sequence of derivative elements in reverse
diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp
index 3dc4f31d0..f267349e4 100644
--- a/src/smt/seq_regex.cpp
+++ b/src/smt/seq_regex.cpp
@@ -323,6 +323,7 @@ namespace smt {
                 literal is_nullable_lit = th.mk_literal(is_nullable);
                 ctx.mark_as_relevant(is_nullable_lit);
                 th.add_axiom(~lit, ~len_s_le_i, is_nullable_lit);
+                th.add_unhandled_expr(is_nullable);
             }
         }