z3str3: fail early on non-string sequence terms

Z3Prover · Oct 1, 2019 · fe7a7fe · fe7a7fe
1 parent d70b63c
commit fe7a7fe
Showing 1 changed file with 4 additions and 0 deletions.
diff --git 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;);
         }