From 5c4f775b1b2b7a9f4b03d2340b36deacd55bea8a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 13 Apr 2020 10:00:42 -0700
Subject: [PATCH] fix #3935

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/automata/symbolic_automata.h     | 3 +++
 src/math/automata/symbolic_automata_def.h | 8 ++++----
 src/smt/theory_seq.cpp                    | 7 ++++---
 3 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/src/math/automata/symbolic_automata.h b/src/math/automata/symbolic_automata.h
index 4831280af7f..0cfdf9bf304 100644
--- a/src/math/automata/symbolic_automata.h
+++ b/src/math/automata/symbolic_automata.h
@@ -120,6 +120,9 @@ class symbolic_automata {
     }
     void generate_min_terms_rec(vector<ref_t> &constraints, vector<std::pair<vector<bool>, ref_t> > &min_terms, unsigned i, vector<bool> &curr_bv, ref_t &curr_pred) {
         lbool is_sat = m_ba.is_sat(curr_pred);
+        if (is_sat == l_undef)
+            throw default_exception("incomplete theory: unable to generate min-terms");
+
         if (is_sat != l_true) {
             return;
         }
diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h
index 4750c6da8a1..5ecdd8c2bd4 100644
--- a/src/math/automata/symbolic_automata_def.h
+++ b/src/math/automata/symbolic_automata_def.h
@@ -44,7 +44,7 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_total
         ref_t cond(m_ba.mk_not(m_ba.mk_or(vs.size(), vs.c_ptr())), m);
         lbool is_sat = m_ba.is_sat(cond);
         if (is_sat == l_undef) {
-            return 0;
+            return nullptr;
         }
         if (is_sat == l_true) {
             new_mvs.push_back(move_t(m, i, dead_state, cond));
@@ -191,7 +191,7 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minim
                                 p1.insert(q);
                                 break;
                             case l_undef:
-                                return 0;
+                                return nullptr;
                             default:
                                 break;
                             }                            
@@ -200,7 +200,7 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minim
                             ref_t psi_min_phi(m_ba.mk_and(psi, m_ba.mk_not(phi)), m);
                             lbool is_sat = m_ba.is_sat(psi_min_phi);
                             if (is_sat == l_undef) {
-                                return 0;
+                                return nullptr;
                             }
                             if (is_sat == l_true) {
                                 psi = psi_min_phi;
@@ -211,7 +211,7 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minim
                             ref_t phi_min_psi(m_ba.mk_and(phi, m_ba.mk_not(psi)), m);
                             is_sat = m_ba.is_sat(phi_min_psi);
                             if (is_sat == l_undef) {
-                                return 0;
+                                return nullptr;
                             }
                             else if (is_sat == l_false) {
                                 p1.insert(q); // psi and phi are equivalent
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 6e26e93f361..70a2ddf4609 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -6366,8 +6366,8 @@ bool theory_seq::is_accept(expr* e, expr*& s, expr*& idx, expr*& re, unsigned& i
         VERIFY(m_autil.is_numeral(to_app(e)->get_arg(3), r));
         SASSERT(r.is_unsigned());
         i = r.get_unsigned();
-        aut = get_automaton(re);
-        return true;
+        aut = get_automaton(re);        
+        return aut != nullptr;
     }
     else {
         return false;
@@ -6444,7 +6444,8 @@ void theory_seq::propagate_accept(literal lit, expr* acc) {
     context& ctx = get_context();
     rational _idx;
     eautomaton* aut = nullptr;
-    VERIFY(is_accept(acc, e, idx, re, src, aut));
+    if (!is_accept(acc, e, idx, re, src, aut))
+        return;
     VERIFY(m_autil.is_numeral(idx, _idx));
     VERIFY(aut);
     if (aut->is_sink_state(src)) {