fix to unit tests

diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 193ba3792e9dec9fa3d7f703d6191393a6bb6bc3..57ce0c78ec73bb090b95a03980f5ed6335cc2421 100644 (file)
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -129,6 +129,7 @@ public:
   void preRegisterTerm(TNode n) {}
   void propagate(Effort level) {}
   void explain(TNode n, Effort level) {}
+  Node getValue(TNode n, TheoryEngine* engine) { return Node::null(); }
   string identify() const { return "DummyTheory"; }
 };
 

diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 4365e7db2067043d8015bd3417b5be14822c94e4..0920fbd56f3a5fa0af9b3959dc67fb06c6cb41dc 100644 (file)
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -205,6 +205,7 @@ public:
   void check(Theory::Effort) { Unimplemented(); }
   void propagate(Theory::Effort) { Unimplemented(); }
   void explain(TNode, Theory::Effort) { Unimplemented(); }
+  Node getValue(TNode n, TheoryEngine* engine) { return Node::null(); }
 };/* class FakeTheory */