From f395c8643cee2ab698462975a6476653a21cd1e9 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Mon, 1 Jun 2020 14:55:44 -0400
Subject: [PATCH] z3str3: construct proper cex for str.at model construction

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

diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp
index 8ebd34245..9da3f3876 100644
--- a/src/smt/theory_str_mc.cpp
+++ b/src/smt/theory_str_mc.cpp
@@ -725,7 +725,10 @@ namespace smt {
             v.init(&get_context());
             rational pos_value;
             bool pos_exists = v.get_value(pos, pos_value);
-            ENSURE(pos_exists);
+            if (!pos_exists) {
+                cex = m.mk_or(m_autil.mk_ge(pos, mk_int(0)), m_autil.mk_le(pos, mk_int(0)));
+                return false;
+            }
             TRACE("str_fl", tout << "reduce str.at: base=" << mk_pp(base, m) << ", pos=" << pos_value.to_string() << std::endl;);
             if (pos_value.is_neg() || pos_value >= rational(base_chars.size())) {
                 // return the empty string