summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDejan Jovanović <dejan.jovanovic@gmail.com>2012-03-26 12:23:54 +0000
committerDejan Jovanović <dejan.jovanovic@gmail.com>2012-03-26 12:23:54 +0000
commit595bc04a19b05541fc1c9351d5bbde7f2d7ba4dc (patch)
treef29ce579e233e05cc2151637b67d88ca51db409e
parent70c23e23c3bfc8aa3fdf285fc643b0438359d22a (diff)
forgot to commit this one, fixing build errors
-rw-r--r--test/unit/prop/cnf_stream_black.h6
1 files changed, 3 insertions, 3 deletions
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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback