mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

use safer mk_and in extended indexof

Browse source
This commit is contained in:
Murphy Berzish 2017-12-06 20:50:03 -05:00
parent b3ebcfe558
commit 9554723b44
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

@ -1330,7 +1330,7 @@ namespace smt {
ite2ElseItems.push_back(ctx.mk_eq_atom(indexAst, mk_indexof(suffix, expr->get_arg(1))));
ite2ElseItems.push_back(ctx.mk_eq_atom(expr->get_arg(2), prefixLen));
ite2ElseItems.push_back(ite3);
expr_ref ite2Else(m.mk_and(ite2ElseItems.size(), ite2ElseItems.c_ptr()), m);
expr_ref ite2Else(mk_and(ite2ElseItems), m);
SASSERT(ite2Else);
expr_ref ite2(m.mk_ite(