From fe7a7fe23fc9190f468766e76e9997ed065a130e Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Mon, 30 Sep 2019 16:27:42 -0400
Subject: [PATCH] z3str3: fail early on non-string sequence terms

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

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 897fe4e45..f4ac682d7 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -8483,6 +8483,10 @@ namespace smt {
                 }
             }
         } else {
+            if (u.str.is_non_string_sequence(ex)) {
+                TRACE("str", tout << "ERROR: Z3str3 does not support non-string sequence terms. Aborting." << std::endl;);
+                m.raise_exception("Z3str3 does not support non-string sequence terms.");
+            }
             TRACE("str", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) <<
                   ": expr is of wrong sort, ignoring" << std::endl;);
         }