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

z3str3: reject certain unhandled expressions (#4818)

Browse source
This commit is contained in:
Murphy Berzish 2020-11-25 14:15:35 -06:00 committed by GitHub
parent c27a325017
commit 6aba325cea
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/smt/theory_str.cpp
View file

@ -6871,6 +6871,13 @@ namespace smt {
family_id m_arith_fid = m.mk_family_id("arith");
sort * int_sort = m.mk_sort(m_arith_fid, INT_SORT);
// reject unhandled expressions
if (u.str.is_replace_all(ex) || u.str.is_replace_re(ex) || u.str.is_replace_re_all(ex) || u.str.is_from_code(ex)
|| u.str.is_to_code(ex) || u.str.is_is_digit(ex)) {
TRACE("str", tout << "ERROR: Z3str3 has encountered an unsupported operator. Aborting." << std::endl;);
m.raise_exception("Z3str3 encountered an unsupported operator.");
}
if (ex_sort == str_sort) {
TRACE("str", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) <<
": expr is of sort String" << std::endl;);