From 9a490befefedfd40b7abab5080e84fb7c0540f86 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Fri, 3 May 2013 16:32:11 -0400
Subject: Fixing compilation of unit tests. These problems were due to
 splitLemma() being pure virtual.

---
 test/unit/theory/theory_engine_white.h | 3 +++
 test/unit/theory/theory_white.h        | 5 +++++
 2 files changed, 8 insertions(+)

(limited to 'test/unit')

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();
-- 
cgit v1.2.3