1 files changed, 24 insertions, 30 deletions

diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 1b8a7c92f..91242322a 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -22,6 +22,8 @@
 #include <string>
 #include <vector>
 
+#include "api/cvc4cpp.h"
+#include "smt/smt_engine.h"
 #include "expr/expr_manager.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
@@ -50,15 +52,13 @@ std::vector<Node> makeNSkolemNodes(NodeManager* nodeManager, int N,
 
 class NodeBlack : public CxxTest::TestSuite {
  private:
-  Options opts;
   NodeManager* d_nodeManager;
-  NodeManagerScope* d_scope;
-  TypeNode* d_booleanType;
-  TypeNode* d_realType;
-
+  api::Solver* d_slv;
  public:
   void setUp() override
   {
+    // setup a SMT engine so that options are in scope
+    Options opts;
     char* argv[2];
     argv[0] = strdup("");
     argv[1] = strdup("--output-lang=ast");
@@ -66,18 +66,12 @@ class NodeBlack : public CxxTest::TestSuite {
     free(argv[0]);
     free(argv[1]);
 
-    d_nodeManager = new NodeManager(NULL, opts);
-    d_scope = new NodeManagerScope(d_nodeManager);
-    d_booleanType = new TypeNode(d_nodeManager->booleanType());
-    d_realType = new TypeNode(d_nodeManager->realType());
+    d_slv = new api::Solver(&opts);
+    d_nodeManager = d_slv->getSmtEngine()->getNodeManager();
   }
 
-  void tearDown() override
-  {
-    delete d_realType;
-    delete d_booleanType;
-    delete d_scope;
-    delete d_nodeManager;
+  void tearDown() override { 
+    delete d_slv;
   }
 
   bool imp(bool a, bool b) const { return (!a) || (b); }
@@ -114,12 +108,12 @@ class NodeBlack : public CxxTest::TestSuite {
   void testOperatorEquals() {
     Node a, b, c;
 
-    b = d_nodeManager->mkSkolem("b", *d_booleanType);
+    b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
 
     a = b;
     c = a;
 
-    Node d = d_nodeManager->mkSkolem("d", *d_booleanType);
+    Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
 
     TS_ASSERT(a == a);
     TS_ASSERT(a == b);
@@ -148,12 +142,12 @@ class NodeBlack : public CxxTest::TestSuite {
   void testOperatorNotEquals() {
     Node a, b, c;
 
-    b = d_nodeManager->mkSkolem("b", *d_booleanType);
+    b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
 
     a = b;
     c = a;
 
-    Node d = d_nodeManager->mkSkolem("d", *d_booleanType);
+    Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
 
     /*structed assuming operator == works */
     TS_ASSERT(iff(a != a, !(a == a)));
@@ -208,7 +202,7 @@ class NodeBlack : public CxxTest::TestSuite {
   void testOperatorAssign() {
     Node a, b;
     Node c = d_nodeManager->mkNode(
-        NOT, d_nodeManager->mkSkolem("c", *d_booleanType));
+        NOT, d_nodeManager->mkSkolem("c", d_nodeManager->booleanType()));
 
     b = c;
     TS_ASSERT(b == c);
@@ -324,8 +318,8 @@ class NodeBlack : public CxxTest::TestSuite {
   void testIteNode() {
     /*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/
 
-    Node a = d_nodeManager->mkSkolem("a", *d_booleanType);
-    Node b = d_nodeManager->mkSkolem("b", *d_booleanType);
+    Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
+    Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
 
     Node cnd = d_nodeManager->mkNode(OR, a, b);
     Node thenBranch = d_nodeManager->mkConst(true);
@@ -383,8 +377,8 @@ class NodeBlack : public CxxTest::TestSuite {
   void testGetKind() {
     /*inline Kind getKind() const; */
 
-    Node a = d_nodeManager->mkSkolem("a", *d_booleanType);
-    Node b = d_nodeManager->mkSkolem("b", *d_booleanType);
+    Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
+    Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
 
     Node n = d_nodeManager->mkNode(NOT, a);
     TS_ASSERT(NOT == n.getKind());
@@ -392,8 +386,8 @@ class NodeBlack : public CxxTest::TestSuite {
     n = d_nodeManager->mkNode(EQUAL, a, b);
     TS_ASSERT(EQUAL == n.getKind());
 
-    Node x = d_nodeManager->mkSkolem("x", *d_realType);
-    Node y = d_nodeManager->mkSkolem("y", *d_realType);
+    Node x = d_nodeManager->mkSkolem("x", d_nodeManager->realType());
+    Node y = d_nodeManager->mkSkolem("y", d_nodeManager->realType());
 
     n = d_nodeManager->mkNode(PLUS, x, y);
     TS_ASSERT(PLUS == n.getKind());
@@ -470,9 +464,9 @@ class NodeBlack : public CxxTest::TestSuite {
   // test iterators
   void testIterator() {
     NodeBuilder<> b;
-    Node x = d_nodeManager->mkSkolem("x", *d_booleanType);
-    Node y = d_nodeManager->mkSkolem("y", *d_booleanType);
-    Node z = d_nodeManager->mkSkolem("z", *d_booleanType);
+    Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+    Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType());
+    Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType());
     Node n = b << x << y << z << kind::AND;
 
     {  // iterator
@@ -717,7 +711,7 @@ class NodeBlack : public CxxTest::TestSuite {
   //  This is for demonstrating what a certain type of user error looks like.
   //   Node level0(){
   //     NodeBuilder<> nb(kind::AND);
-  //     Node x = d_nodeManager->mkSkolem("x", *d_booleanType);
+  //     Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
   //     nb << x;
   //     nb << x;
   //     return Node(nb.constructNode());