From: Dejan Jovanović 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; }