From cf1a600fb981bfae72dd895e9fef9a9f79f3c5fb Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 27 Mar 2014 13:37:04 +0000
Subject: [PATCH] bugfix

---
 src/tactic/sls/sls_engine.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp
index cc06e4f78..10aaf6601 100644
--- a/src/tactic/sls/sls_engine.cpp
+++ b/src/tactic/sls/sls_engine.cpp
@@ -1061,13 +1061,13 @@ lbool sls_engine::search_old() {
             }
         }
     }
-#endif
 
 bailout:
     m_mpz_manager.del(new_value);
 
     return res;
 }
+#endif
 
 void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) {
     if (g->inconsistent()) {