From 076870174415958c9b0c975758503f8ff9cf4417 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 10 Mar 2020 16:08:16 -0700
Subject: [PATCH] fix #3220

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_solver.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 5c7d7b8df..39217f6f0 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1279,6 +1279,7 @@ namespace sat {
     };
 
     lbool solver::invoke_local_search(unsigned num_lits, literal const* lits) {
+        if (inconsistent()) return l_false;
         scoped_limits scoped_rl(rlimit());
         SASSERT(m_local_search);
         i_local_search& srch = *m_local_search;