Some SAT stuff, not doing anything special yet, just to keep it in sync.

2 files changed, 7 insertions, 3 deletions

diff --git a/src/prop/minisat/simp/SimpSolver.C b/src/prop/minisat/simp/SimpSolver.C
index 063332e74..124849155 100644
--- a/src/prop/minisat/simp/SimpSolver.C
+++ b/src/prop/minisat/simp/SimpSolver.C
@@ -28,8 +28,9 @@ namespace CVC4 {
 namespace prop {
 namespace minisat {
 
-SimpSolver::SimpSolver() :
-    grow               (0)
+SimpSolver::SimpSolver(SatSolver* proxy, context::Context* context) :
+    Solver(proxy, context)
+  , grow               (0)
   , asymm_mode         (false)
   , redundancy_check   (false)
   , merges             (0)
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index 223b21998..67d0d2b95 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -30,13 +30,16 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 namespace CVC4 {
 namespace prop {
+
+class SatSolver;
+
 namespace minisat {
 
 class SimpSolver : public Solver {
  public:
     // Constructor/Destructor:
     //
-    SimpSolver();
+    SimpSolver(SatSolver* proxy, context::Context* context);
     CVC4_PUBLIC ~SimpSolver();
 
     // Problem specification: