From 7ddb940f77582babb2cd1e799c7c2f815bb80b82 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Wed, 19 Jul 2017 10:15:38 -0400
Subject: [PATCH] add e_internalized() check in theory_str::get_arith_value()

---
 src/smt/theory_str.cpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 1007ee662..89e0123a8 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -4656,6 +4656,11 @@ namespace smt {
         context& ctx = get_context();
         ast_manager & m = get_manager();
 
+	// safety
+	if (!ctx.e_internalized(e)) {
+	  return false;
+	}
+	
         // if an integer constant exists in the eqc, it should be the root
         enode * en_e = ctx.get_enode(e);
         enode * root_e = en_e->get_root();