mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

z3str2 eqc semantics for theory_str unroll checks

Browse source
This commit is contained in:
Murphy Berzish 2016-09-13 18:24:59 -04:00
parent 8f636e1f57
commit 34dc655150
1 changed files with 2 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_str.cpp
View file

@ -8883,9 +8883,7 @@ void theory_str::get_eqc_allUnroll(expr * n, expr * &constStr, std::set<expr*> &
unrollFuncSet.insert(curr);
}
}
enode * e_curr = ctx.get_enode(curr);
curr = e_curr->get_next()->get_owner();
// curr = get_eqc_next(t, curr);
curr = get_eqc_next(curr);
} while (curr != n);
}
@ -8907,9 +8905,7 @@ void theory_str::get_eqc_simpleUnroll(expr * n, expr * &constStr, std::set<expr*
}
}
}
enode * e_curr = ctx.get_enode(curr);
curr = e_curr->get_next()->get_owner();
// curr = get_eqc_next(t, curr);
curr = get_eqc_next(curr);
} while (curr != n);
}