mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

#7344

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-08-26 14:22:28 -07:00
parent 84da614de3
commit 349ebd0a5b
3 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/smt/smt_context.cpp
View file

@ -1858,8 +1858,10 @@ namespace smt {
lbool phase = l_undef; lbool phase = l_undef;
m_case_split_queue->next_case_split(var, phase); m_case_split_queue->next_case_split(var, phase);
used_queue = true; used_queue = true;
if (var == null_bool_var) if (var == null_bool_var) {
push_trail(value_trail(m_has_case_split, false));
return false; return false;
}
TRACE_CODE({ TRACE_CODE({
static unsigned counter = 0; static unsigned counter = 0;
@ -4642,6 +4644,9 @@ namespace smt {
} }
bool context::has_case_splits() { bool context::has_case_splits() {
if (!m_has_case_split)
return false;
for (unsigned i = get_num_b_internalized(); i-- > 0; ) { for (unsigned i = get_num_b_internalized(); i-- > 0; ) {
if (is_relevant(i) && get_assignment(i) == l_undef) if (is_relevant(i) && get_assignment(i) == l_undef)
return true; return true;

1
src/smt/smt_context.h
View file

@ -1155,6 +1155,7 @@ namespace smt {
bool guess(bool_var var, lbool phase); bool guess(bool_var var, lbool phase);
protected: protected:
bool m_has_case_split = true;
bool decide(); bool decide();
void update_phase_cache_counter(); void update_phase_cache_counter();

1
src/smt/smt_model_generator.cpp
View file

@ -99,7 +99,6 @@ namespace smt {
if (m.is_bool(s)) { if (m.is_bool(s)) {
CTRACE("model", m_context->get_assignment(r) == l_undef, CTRACE("model", m_context->get_assignment(r) == l_undef,
tout << mk_pp(r->get_expr(), m) << "\n";); tout << mk_pp(r->get_expr(), m) << "\n";);
SASSERT(m_context->get_assignment(r) != l_undef);
if (m_context->get_assignment(r) == l_true) if (m_context->get_assignment(r) == l_true)
proc = alloc(expr_wrapper_proc, m.mk_true()); proc = alloc(expr_wrapper_proc, m.mk_true());
else else