mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 14:43:23 +00:00
Code Activity

Merge pull request #4490 from mtrberzi/issue4486

Browse source 
z3str3: construct proper cex for str.at model construction
This commit is contained in:
Murphy Berzish 2020-06-01 20:06:51 -05:00 • committed by GitHub
commit 99f20c59e4
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_str_mc.cpp
View file

@ -725,7 +725,10 @@ namespace smt {
v.init(&get_context()); v.init(&get_context());
rational pos_value; rational pos_value;
bool pos_exists = v.get_value(pos, pos_value); bool pos_exists = v.get_value(pos, pos_value);
ENSURE(pos_exists); if (!pos_exists) {
cex = m.mk_or(m_autil.mk_ge(pos, mk_int(0)), m_autil.mk_le(pos, mk_int(0)));
return false;
}
TRACE("str_fl", tout << "reduce str.at: base=" << mk_pp(base, m) << ", pos=" << pos_value.to_string() << std::endl;); TRACE("str_fl", tout << "reduce str.at: base=" << mk_pp(base, m) << ", pos=" << pos_value.to_string() << std::endl;);
if (pos_value.is_neg() || pos_value >= rational(base_chars.size())) { if (pos_value.is_neg() || pos_value >= rational(base_chars.size())) {
// return the empty string // return the empty string