Fixing compilation of unit tests. These problems were due to splitLemma() being pure virtual.

2 files changed, 8 insertions, 0 deletions

diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index c9bea1795..4035b85da 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -76,6 +76,9 @@ class FakeOutputChannel : public OutputChannel {
   void handleUserAttribute( const char* attr, Theory* t ){
     Unimplemented();
   }
+  LemmaStatus splitLemma(TNode n, bool removable) throw(TypeCheckingExceptionPrivate, AssertionException){
+    Unimplemented();
+  }
 };/* class FakeOutputChannel */
 
 template<TheoryId theory>
diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index 126f57060..d9df2912b 100644
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -76,6 +76,11 @@ public:
     return LemmaStatus(Node::null(), 0);
   }
 
+  LemmaStatus splitLemma(TNode n, bool removable) throw (TypeCheckingExceptionPrivate, AssertionException){
+    push(LEMMA, n);
+    return LemmaStatus(Node::null(), 0);
+  }
+
   void requirePhase(TNode, bool)
     throw(Interrupted, AssertionException) {
     Unreachable();