diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 70b55acee..be4e8321f 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3186,6 +3186,7 @@ namespace smt { if (m_tmp_clauses.empty()) return l_true; for (auto & tmp_clause : m_tmp_clauses) { literal_vector& lits = tmp_clause.second; + literal unassigned = null_literal; for (literal l : lits) { switch (get_assignment(l)) { case l_false: @@ -3193,13 +3194,17 @@ namespace smt { case l_true: goto next_clause; default: - shuffle(lits.size(), lits.c_ptr(), m_random); - push_scope(); - assign(l, b_justification::mk_axiom(), true); - return l_undef; + unassigned = l; } } + if (unassigned != null_literal) { + shuffle(lits.size(), lits.c_ptr(), m_random); + push_scope(); + assign(unassigned, b_justification::mk_axiom(), true); + return l_undef; + } + if (lits.size() == 1) { set_conflict(b_justification(), ~lits[0]); }