Fix theory white unit test (#5194)

diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index 707255b05548abe62d30b5703b7c2341ea3fdc6f..552aeb3c688f13e7f9120e20315897deb6cbefcb 100644 (file)
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -100,9 +100,18 @@ class DummyTheory : public Theory {
               Valuation valuation,
               const LogicInfo& logicInfo,
               ProofNodeManager* pnm)
-      : Theory(
-            theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo, pnm)
-  {}
+      : Theory(theory::THEORY_BUILTIN,
+               ctxt,
+               uctxt,
+               out,
+               valuation,
+               logicInfo,
+               pnm),
+        d_state(ctxt, uctxt, valuation)
+  {
+    // use a default theory state object
+    d_theoryState = &d_state;
+  }
 
   TheoryRewriter* getTheoryRewriter() { return nullptr; }
 
@@ -128,19 +137,20 @@ class DummyTheory : public Theory {
     return done();
   }
 
-  void check(Effort e) override
-  {
-    while(!done()) {
-      getWrapper();
-    }
-  }
-
   void presolve() override { Unimplemented(); }
   void preRegisterTerm(TNode n) override {}
   void propagate(Effort level) override {}
+  bool preNotifyFact(
+      TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal) override
+  {
+    // do not assert to equality engine, since this theory does not use one
+    return true;
+  }
   TrustNode explain(TNode n) override { return TrustNode::null(); }
   Node getValue(TNode n) { return Node::null(); }
   string identify() const override { return "DummyTheory"; }
+  /** Default theory state object */
+  TheoryState d_state;
 };/* class DummyTheory */
 
 class TheoryBlack : public CxxTest::TestSuite {