mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

z3str3: fail early on non-string sequence terms

Browse source
This commit is contained in:
Murphy Berzish 2019-09-30 16:27:42 -04:00 committed by Nikolaj Bjorner
parent d70b63c8ac
commit fe7a7fe23f
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_str.cpp
View file

@ -8483,6 +8483,10 @@ namespace smt {
} }
} }
} else { } 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()) << TRACE("str", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) <<
": expr is of wrong sort, ignoring" << std::endl;); ": expr is of wrong sort, ignoring" << std::endl;);
} }