address some crashes reported by Caleb

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Jun 21, 2020 · 02f34ea · 02f34ea
1 parent 6524a70
commit 02f34ea
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 4 deletions.
diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp
@@ -525,7 +525,8 @@ namespace smt {
             lits.reset();
             lits.push_back(~lit);
             if (!m.is_true(cond)) {
-                lits.push_back(th.mk_literal(mk_forall(m, hd, mk_not(m, cond))));
+                expr_ref ncond(mk_not(m, cond), m);
+                lits.push_back(th.mk_literal(mk_forall(m, hd, ncond)));
             }
             expr_ref is_empty1 = sk().mk_is_empty(p.second, re().mk_union(u, r));    
             lits.push_back(th.mk_literal(is_empty1)); 

diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp
@@ -128,7 +128,7 @@ namespace smt {
 
     enode* theory::ensure_enode(expr* e) {
         if (!ctx.e_internalized(e)) {
-            ctx.internalize(e, false);
+            ctx.internalize(e, is_quantifier(e));
         }
         enode* n = ctx.get_enode(e);
         ctx.mark_as_relevant(n);

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
@@ -720,7 +720,7 @@ bool theory_seq::is_solved() {
     }
 
 #if 0
-	// debug code
+    // debug code
     for (enode* n : ctx.enodes()) {
         expr* e = nullptr;
         rational len1, len2;
@@ -2881,8 +2881,11 @@ literal theory_seq::mk_simplified_literal(expr * _e) {
 literal theory_seq::mk_literal(expr* _e) {
     expr_ref e(_e, m);
     bool is_not = m.is_not(_e, _e);
-    ensure_enode(_e);
+    if (!ctx.e_internalized(_e)) {
+        ctx.internalize(_e, is_quantifier(_e));
+    }
     literal lit = ctx.get_literal(_e);
+    ctx.mark_as_relevant(lit);
     if (is_not) lit.neg();
     return lit;
 }