From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 9 Oct 2010 06:16:29 +0000 (+0000)
Subject: fix to unit tests
X-Git-Tag: cvc5-1.0.0~8815
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ec86769172d29ff7f5ed959866ecef339264552b;p=cvc5.git

fix to unit tests
---

diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 193ba3792..57ce0c78e 100644
--- 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 4365e7db2..0920fbd56 100644
--- 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 */