From 02f34ea4b1ba339f58a940116891a2895e10cde0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 20 Jun 2020 18:35:16 -0700
Subject: [PATCH] address some crashes reported by Caleb

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/seq_regex.cpp  | 3 ++-
 src/smt/smt_theory.cpp | 2 +-
 src/smt/theory_seq.cpp | 7 +++++--
 3 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp
index c10a4ded2..9688e4648 100644
--- 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
index 5e11e7a66..21abd7e90 100644
--- 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
index 1ec005ac8..0ba9e7851 100644
--- 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;
 }