From 6b0e599b889da947140a1c36b8bd4360284b4bb7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 5 Mar 2020 11:22:13 +0100
Subject: [PATCH] fix #3140

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_local_search.cpp | 4 ++--
 src/sat/sat_solver.cpp       | 1 +
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp
index 8465b4abe..64aeaaa33 100644
--- a/src/sat/sat_local_search.cpp
+++ b/src/sat/sat_local_search.cpp
@@ -581,7 +581,6 @@ namespace sat {
             m_vars[m_units[i]].m_unit = false;
         }
         m_units.shrink(num_units); 
-        m_vars.pop_back();  // remove sentinel variable
 
         TRACE("sat", display(tout););
 
@@ -597,6 +596,7 @@ namespace sat {
         else {
             result = l_undef;
         }
+        m_vars.pop_back();  // remove sentinel variable
         IF_VERBOSE(1, verbose_stream() << "(sat.local-search " << result << ")\n";);
         IF_VERBOSE(20, display(verbose_stream()););
         return result;
@@ -638,7 +638,7 @@ namespace sat {
             propagate(~best);
         }        
         else {
-            std::cout << "no best\n";
+            IF_VERBOSE(1, verbose_stream() << "(sat.local-search no best)\n");
         }
     }
 
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index b6ad3eb98..5c7d7b8df 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1288,6 +1288,7 @@ namespace sat {
         lbool r = srch.check(num_lits, lits, nullptr);
         if (r == l_true) {
             m_model = srch.get_model();
+            m_model_is_current = true;
         }
         m_local_search = nullptr;
         dealloc(&srch);