From 847a5fc1f82b437b46db0d9cc8b813560141050f Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Thu, 7 Jul 2016 16:13:48 -0400
Subject: [PATCH] replace old mk_value behaviour in theory_str that creates
 placeholders for unused terms instead of crashing

---
 src/smt/theory_str.cpp | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index c28132feb..0626c6ac5 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -6844,8 +6844,7 @@ model_value_proc * theory_str::mk_value(enode * n, model_generator & mg) {
         TRACE("t_str", tout << "WARNING: failed to find a concrete value, falling back" << std::endl;);
         // TODO make absolutely sure the reason we can't find a concrete value is because of an unassigned temporary
         // e.g. for an expression like (Concat X $$_str0)
-        //return alloc(expr_wrapper_proc, m_strutil.mk_string("**UNUSED**"));
-        NOT_IMPLEMENTED_YET();
+        return alloc(expr_wrapper_proc, m_strutil.mk_string("**UNUSED**"));
     }
 }