3 files changed, 17 insertions, 7 deletions
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index 8afc012ff..c07fb1b09 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -26,7 +26,7 @@
 #include "expr/node_manager.h"
 #include "expr/attribute.h"
 #include "expr/node.h"
-#include "theory/theory.h"
+#include "theory/theory_engine.h"
 #include "theory/uf/theory_uf.h"
 #include "util/Assert.h"
 
@@ -138,8 +138,17 @@ public:
     TS_ASSERT_DIFFERS(theory::Theory::RegisteredAttr::s_id, TestFlag2cd::s_id);
     TS_ASSERT_DIFFERS(TestFlag1cd::s_id, TestFlag2cd::s_id);
 
-    lastId = attr::LastAttributeId<TNode, false>::s_id;
-    TS_ASSERT_LESS_THAN(theory::RewriteCache::s_id, lastId);
+    lastId = attr::LastAttributeId<Node, false>::s_id;
+    TS_ASSERT_LESS_THAN(theory::PreRewriteCache::s_id, lastId);
+    TS_ASSERT_LESS_THAN(theory::PostRewriteCache::s_id, lastId);
+    TS_ASSERT_LESS_THAN(theory::PreRewriteCacheTop::s_id, lastId);
+    TS_ASSERT_LESS_THAN(theory::PostRewriteCacheTop::s_id, lastId);
+    TS_ASSERT_DIFFERS(theory::PreRewriteCache::s_id, theory::PostRewriteCache::s_id);
+    TS_ASSERT_DIFFERS(theory::PreRewriteCache::s_id, theory::PreRewriteCacheTop::s_id);
+    TS_ASSERT_DIFFERS(theory::PreRewriteCache::s_id, theory::PostRewriteCacheTop::s_id);
+    TS_ASSERT_DIFFERS(theory::PostRewriteCache::s_id, theory::PreRewriteCacheTop::s_id);
+    TS_ASSERT_DIFFERS(theory::PostRewriteCache::s_id, theory::PostRewriteCacheTop::s_id);
+    TS_ASSERT_DIFFERS(theory::PreRewriteCacheTop::s_id, theory::PostRewriteCacheTop::s_id);
 
     lastId = attr::LastAttributeId<TypeNode, false>::s_id;
     TS_ASSERT_LESS_THAN(NodeManager::TypeAttr::s_id, lastId);
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index fe9cbb388..d6614b87e 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -206,7 +206,7 @@ public:
 
 
     Node expectedProp = d_nm->mkNode(GEQ, x, c);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), PROPOGATE);
+    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), PROPAGATE);
     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), expectedProp);
 
   }
@@ -236,7 +236,7 @@ public:
     d_arith->explain(rLeq1, d_level);
 
     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), PROPOGATE);
+    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), PROPAGATE);
     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), EXPLANATION);
     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq1);
     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), rLt1);
@@ -270,8 +270,8 @@ public:
     d_arith->explain(rLeq1, d_level);
 
     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 4u);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), PROPOGATE);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), PROPOGATE);
+    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), PROPAGATE);
+    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), PROPAGATE);
     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), EXPLANATION);
     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(3), EXPLANATION);
 
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 9c056d368..106d01b13 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) {}
+  string identify() const { return "DummyTheory"; }
 };
 
 class TheoryBlack : public CxxTest::TestSuite {