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

theory_str cleanup

Browse source
This commit is contained in:
Murphy Berzish 2016-08-31 19:19:23 -04:00
parent 89d5f4ffb4
commit 5e22bc57c8
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_str.cpp
View file

@ -3401,7 +3401,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) {
std::string part2Str = strValue.substr(i, strValue.size() - i);
expr_ref cropStr(m_strutil.mk_string(part1Str), mgr);
expr_ref suffixStr(m_strutil.mk_string(part2Str), mgr);
expr_ref y_concat(mk_concat(suffixStr, n), mgr); // TODO concat axioms?
expr_ref y_concat(mk_concat(suffixStr, n), mgr);
if (can_two_nodes_eq(x, cropStr) && can_two_nodes_eq(y, y_concat)) {
// break down option 3-1
@ -6435,6 +6435,7 @@ void theory_str::push_scope_eh() {
void theory_str::pop_scope_eh(unsigned num_scopes) {
sLevel -= num_scopes;
TRACE("t_str", tout << "pop " << num_scopes << " to " << sLevel << std::endl;);
TRACE("t_str_dump_assign_on_scope_change", dump_assignments(););
std::map<expr*, std::stack<T_cut *> >::iterator varItor = cut_var_map.begin();
while (varItor != cut_var_map.end()) {