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

add cut var info for theory_str processtype2

Browse source
This commit is contained in:
Murphy Berzish 2017-02-07 14:41:16 -05:00
parent 19779f1a9b
commit 55cb440aae
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_str.cpp
View file

@ -3648,7 +3648,7 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) {
add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true);
} else {
TRACE("t_str", tout << "AVOID LOOP: SKIP" << std::endl;);
// TODO printCutVar(m, y);
TRACE("t_str_detail", {print_cut_var(m, tout); print_cut_var(y, tout);});
}
}
}
@ -3756,7 +3756,7 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) {
add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true);
} else {
TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;);
// TODO printCutVar(m, y)
TRACE("t_str_detail", {print_cut_var(m, tout); print_cut_var(y, tout);});
}
}
}