mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

fix #3436

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-22 13:02:08 -07:00
parent 94234aef97
commit 00520041fe
2 changed files with 11 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/smt/smt_context.cpp
View file

@ -1947,6 +1947,7 @@ namespace smt {
m_region.push_scope();
m_scopes.push_back(scope());
scope & s = m_scopes.back();
TRACE("context", tout << "push " << m_scope_lvl << "\n";);
m_relevancy_propagator->push();
s.m_assigned_literals_lim = m_assigned_literals.size();
@ -3357,7 +3358,9 @@ namespace smt {
\brief Execute some finalization code after performing the search.
*/
lbool context::check_finalize(lbool r) {
TRACE("after_search", display(tout << "result: " << r << "\n"););
TRACE("after_search", display(tout << "result: " << r << "\n");
m_case_split_queue->display(tout << "case splits\n");
);
display_profile(verbose_stream());
if (r == l_true && get_cancel_flag()) {
r = l_undef;
@ -3584,7 +3587,7 @@ namespace smt {
}
void context::end_search() {
m_case_split_queue ->end_search_eh();
m_case_split_queue->end_search_eh();
}
void context::inc_limits() {
@ -4503,10 +4506,11 @@ namespace smt {
}
bool context::has_case_splits() {
bool_var var;
lbool phase = l_undef;
m_case_split_queue->next_case_split(var, phase);
return (var != null_bool_var);
for (unsigned i = get_num_b_internalized(); i-- > 0; ) {
if (get_assignment(i) == l_undef)
return true;
}
return false;
}
void context::get_model(model_ref & m) {

2
src/smt/smt_internalizer.cpp
View file

@ -420,13 +420,13 @@ namespace smt {
\brief Internalize an equality.
*/
void context::internalize_eq(app * n, bool gate_ctx) {
TRACE("internalize", tout << mk_pp(n, m) << "\n";);
SASSERT(!b_internalized(n));
SASSERT(m.is_eq(n));
internalize_formula_core(n, gate_ctx);
bool_var v = get_bool_var(n);
bool_var_data & d = get_bdata(v);
d.set_eq_flag();
TRACE("internalize", tout << mk_pp(n, m) << " " << literal(v, false) << "\n";);
sort * s = m.get_sort(n->get_arg(0));
theory * th = m_theories.get_plugin(s->get_family_id());