From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Mon, 26 Mar 2012 12:23:54 +0000 (+0000)
Subject: forgot to commit this one, fixing build errors
X-Git-Tag: cvc5-1.0.0~8265
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=595bc04a19b05541fc1c9351d5bbde7f2d7ba4dc;p=cvc5.git

forgot to commit this one, fixing build errors
---

diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index e9cba5f9c..d1f79f6ab 100644
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -28,7 +28,7 @@
 #include "context/context.h"
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
-#include "prop/sat.h"
+#include "prop/theory_proxy.h"
 #include "smt/smt_engine.h"
 
 #include "theory/theory.h"
@@ -45,7 +45,7 @@ using namespace CVC4::prop;
 using namespace std;
 
 /* This fake class relies on the face that a MiniSat variable is just an int. */
-class FakeSatSolver : public SatSolverInterface {
+class FakeSatSolver : public SatSolver {
   SatVariable d_nextVar;
   bool d_addClauseCalled;
 
@@ -71,7 +71,7 @@ public:
     return d_addClauseCalled;
   }
 
-  int getAssertionLevel() const {
+  unsigned getAssertionLevel() const {
     return 0;
   }