From ddc77b11005b6e924229638a88ea0fdaf2f113ed Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 31 Mar 2020 20:53:10 -0700
Subject: [PATCH] fix #3632
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/sat/sat_local_search.cpp | 16 +++++++++++++---
src/sat/sat_solver.cpp | 5 ++++-
2 files changed, 17 insertions(+), 4 deletions(-)
diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp
index dc2193168..b3ce9c6c1 100644
--- a/src/sat/sat_local_search.cpp
+++ b/src/sat/sat_local_search.cpp
@@ -31,7 +31,9 @@ namespace sat {
for (unsigned i = 0; i < m_assumptions.size(); ++i) {
add_clause(1, m_assumptions.c_ptr() + i);
}
-
+ if (m_is_unsat)
+ return;
+
// add sentinel variable.
m_vars.push_back(var_info());
@@ -334,7 +336,12 @@ namespace sat {
void local_search::add_unit(literal lit, literal exp) {
bool_var v = lit.var();
- if (is_unit(lit)) return;
+ if (is_unit(lit)) {
+ if (m_vars[v].m_value == lit.sign()) {
+ m_is_unsat = true;
+ }
+ return;
+ }
SASSERT(!m_units.contains(v));
if (m_vars[v].m_value == lit.sign() && !m_initializing) {
flip_walksat(v);
@@ -575,8 +582,11 @@ namespace sat {
m_assumptions.append(sz, assumptions);
unsigned num_units = m_units.size();
init();
+ if (m_is_unsat)
+ return l_false;
walksat();
-
+
+ TRACE("sat", tout << m_units << "\n";);
// remove unit clauses
for (unsigned i = m_units.size(); i-- > num_units; ) {
m_vars[m_units[i]].m_unit = false;
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 0d6edd3ab..fc7ce0837 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1282,7 +1282,10 @@ namespace sat {
struct scoped_ls {
solver& s;
scoped_ls(solver& s): s(s) {}
- ~scoped_ls() { dealloc(s.m_local_search); s.m_local_search = nullptr; }
+ ~scoped_ls() {
+ dealloc(s.m_local_search);
+ s.m_local_search = nullptr;
+ }
};
scoped_ls _ls(*this);
if (inconsistent()) return l_false;