mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

improve error message in theory_str when an invalid term in str.to.re is encountered

Browse source 
addresses #871
This commit is contained in:
Murphy Berzish 2017-08-18 17:31:40 -04:00
parent b2388464e4
commit 1e445a62d4
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_str.cpp
View file

@ -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;
}