mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

z3str3: negative lengths in get_len_value don't count

Browse source
This commit is contained in:
Murphy Berzish 2019-11-25 14:28:44 -05:00 • committed by Nikolaj Bjorner
parent 58f3dce2be
commit 5f78ca9b58
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_str.cpp
View file

@ -5061,7 +5061,7 @@ namespace smt {
}
TRACE("str", tout << "length of " << mk_ismt2_pp(e, m) << " is " << val << std::endl;);
return val.is_int();
return val.is_int() && val.is_nonneg();
}
/*