From 8373bec6ad0bc2c91bd09319ad187fd7f7821e17 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 9 Jul 2018 10:33:56 -0700 Subject: [PATCH] only assign, if there isn't already a true literal incube/clause mode Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) 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]); }