mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-08 12:11:23 +00:00
Code Activity

Remove unused iPos.

Browse source 
This was incremented, but never actually used, so remove it.
This commit is contained in:
Bruce Mitchener 2018-11-30 23:13:22 +07:00
parent c51caad5ad
commit 2faf5ef995
1 changed files with 0 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_str.cpp
View file

@ -7501,15 +7501,12 @@ namespace smt {
expr_ref newConcat(m); expr_ref newConcat(m);
if (arg1 != a1 || arg2 != a2) { if (arg1 != a1 || arg2 != a2) {
TRACE("str", tout << "resolved concat argument(s) to eqc string constants" << std::endl;); TRACE("str", tout << "resolved concat argument(s) to eqc string constants" << std::endl;);
int iPos = 0;
expr_ref_vector item1(m); expr_ref_vector item1(m);
if (a1 != arg1) { if (a1 != arg1) {
item1.push_back(ctx.mk_eq_atom(a1, arg1)); item1.push_back(ctx.mk_eq_atom(a1, arg1));
iPos += 1;
} }
if (a2 != arg2) { if (a2 != arg2) {
item1.push_back(ctx.mk_eq_atom(a2, arg2)); item1.push_back(ctx.mk_eq_atom(a2, arg2));
iPos += 1;
} }
expr_ref implyL1(mk_and(item1), m); expr_ref implyL1(mk_and(item1), m);
newConcat = mk_concat(arg1, arg2); newConcat = mk_concat(arg1, arg2);