From 1e445a62d4d37009cdd537d22bff2d0826efcf1d Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Fri, 18 Aug 2017 17:31:40 -0400
Subject: [PATCH] improve error message in theory_str when an invalid term in
 str.to.re is encountered

addresses #871
---
 src/smt/theory_str.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 5642339f4..7fbc15e8a 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -6223,7 +6223,8 @@ namespace smt {
                     TRACE("str", tout << "string transition " << last << "--" << str[(str.length() - 1)] << "--> " << end << "\n";);
                 }
             } else { // ! u.str.is_string(arg_str, str)
-                TRACE("str", tout << "invalid string constant in Str2Reg" << std::endl;);
+                TRACE("str", tout << "WARNING: invalid string constant in str.to.re! Cancelling." << std::endl;);
+                u.get_manager().raise_exception("invalid term in str.to.re, argument must be a string constant");
                 m_valid = false;
                 return;
             }