diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-26 12:23:54 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-26 12:23:54 +0000 |
commit | 595bc04a19b05541fc1c9351d5bbde7f2d7ba4dc (patch) | |
tree | f29ce579e233e05cc2151637b67d88ca51db409e /test | |
parent | 70c23e23c3bfc8aa3fdf285fc643b0438359d22a (diff) |
forgot to commit this one, fixing build errors
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/prop/cnf_stream_black.h | 6 |
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; } |