From eaf75336485859e726b344bad789b5e63a430ff2 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 6 Nov 2010 10:14:06 +0000
Subject: [PATCH] Bugfix. simplifying-minisat failed when
 abstraction/refinement was turned on. The elminate() function needs to be
 called.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1026 e59a4935-1847-0410-ae03-e826735625c1
---
 src/sat/MinisatCore.cpp        | 2 ++
 src/sat/SimplifyingMinisat.cpp | 4 +++-
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/sat/MinisatCore.cpp b/src/sat/MinisatCore.cpp
index 236190a..e90b10b 100644
--- a/src/sat/MinisatCore.cpp
+++ b/src/sat/MinisatCore.cpp
@@ -1,6 +1,7 @@
 #include "core/Solver.h"
 #include "MinisatCore.h"
 #include "utils/System.h"
+#include "simp/SimpSolver.h"
 
 namespace BEEV
 {
@@ -85,4 +86,5 @@ namespace BEEV
   // I was going to make SimpSolver and Solver instances of this template.
   // But I'm not so sure now because I don't understand what eliminate() does in the simp solver.
   template class MinisatCore<Minisat::Solver>;
+  template class MinisatCore<Minisat::SimpSolver>;
 };
diff --git a/src/sat/SimplifyingMinisat.cpp b/src/sat/SimplifyingMinisat.cpp
index a106f56..e1e1115 100644
--- a/src/sat/SimplifyingMinisat.cpp
+++ b/src/sat/SimplifyingMinisat.cpp
@@ -6,7 +6,7 @@ namespace BEEV
 {
   SimplifyingMinisat::SimplifyingMinisat()
   {
-    s = new Minisat::SimpSolver();
+	 s = new Minisat::SimpSolver();
   }
 
   SimplifyingMinisat::~SimplifyingMinisat()
@@ -32,6 +32,8 @@ namespace BEEV
     if (!s->simplify())
       return false;
 
+    // Without the eliminate(true) call. Calling solve() multiple times returns the wrong answer.
+	s->eliminate(true);
     return s->solve();
   }
 
-- 
2.47.3