From 42fbe19814cdb25d450b4e222252a6ded6361fa0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 21 Oct 2017 18:56:36 -0400
Subject: [PATCH] fix #1316, segmentation fault when numeric value is not
 internalized

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_seq.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 44ce804e7..d55484384 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -3466,6 +3466,8 @@ static bool get_arith_value(context& ctx, theory_id afid, expr* e, expr_ref& v)
 bool theory_seq::get_num_value(expr* e, rational& val) const {
     context& ctx = get_context();
     expr_ref _val(m);
+	if (!ctx.e_internalized(e))
+		return false;
     enode* next = ctx.get_enode(e), *n = next;
     do { 
         if (get_arith_value(ctx, m_autil.get_family_id(), next->get_owner(), _val) && m_autil.is_numeral(_val, val) && val.is_int()) {