fix #3935

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Apr 13, 2020 · 5c4f775 · 5c4f775
1 parent 01c12c9
commit 5c4f775
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 7 deletions.
diff --git 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
@@ -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
@@ -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)) {