New C++ API: Keep reference to solver object in non-solver objects. (#4549)

This is in preparation for adding guards to ensure that sort and term
arguments belong to the same solver.

3 files changed, 11 insertions, 11 deletions

diff --git a/test/unit/api/op_black.h b/test/unit/api/op_black.h
index e99e8daf2..27ca7bb88 100644
--- a/test/unit/api/op_black.h
+++ b/test/unit/api/op_black.h
@@ -52,7 +52,7 @@ void OpBlack::testIsNull()
 
 void OpBlack::testOpFromKind()
 {
-  Op plus(PLUS);
+  Op plus(&d_solver, PLUS);
   TS_ASSERT(!plus.isIndexed());
   TS_ASSERT_THROWS(plus.getIndices<uint32_t>(), CVC4ApiException&);
 
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 07b5c5aec..90d4c10c1 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -978,13 +978,13 @@ void SolverBlack::testGetOp()
   Term listhead = d_solver->mkTerm(APPLY_SELECTOR, headTerm, listcons1);
 
   TS_ASSERT(listnil.hasOp());
-  TS_ASSERT_EQUALS(listnil.getOp(), APPLY_CONSTRUCTOR);
+  TS_ASSERT_EQUALS(listnil.getOp(), Op(d_solver.get(), APPLY_CONSTRUCTOR));
 
   TS_ASSERT(listcons1.hasOp());
-  TS_ASSERT_EQUALS(listcons1.getOp(), APPLY_CONSTRUCTOR);
+  TS_ASSERT_EQUALS(listcons1.getOp(), Op(d_solver.get(), APPLY_CONSTRUCTOR));
 
   TS_ASSERT(listhead.hasOp());
-  TS_ASSERT_EQUALS(listhead.getOp(), APPLY_SELECTOR);
+  TS_ASSERT_EQUALS(listhead.getOp(), Op(d_solver.get(), APPLY_SELECTOR));
 }
 
 void SolverBlack::testPush1()
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index 78d6ee5cc..d8f022201 100644
--- a/test/unit/api/term_black.h
+++ b/test/unit/api/term_black.h
@@ -175,10 +175,10 @@ void TermBlack::testGetOp()
   Term extb = d_solver.mkTerm(ext, b);
 
   TS_ASSERT(ab.hasOp());
-  TS_ASSERT_EQUALS(ab.getOp(), Op(SELECT));
+  TS_ASSERT_EQUALS(ab.getOp(), Op(&d_solver, SELECT));
   TS_ASSERT(!ab.getOp().isIndexed());
   // can compare directly to a Kind (will invoke Op constructor)
-  TS_ASSERT_EQUALS(ab.getOp(), SELECT);
+  TS_ASSERT_EQUALS(ab.getOp(), Op(&d_solver, SELECT));
   TS_ASSERT(extb.hasOp());
   TS_ASSERT(extb.getOp().isIndexed());
   TS_ASSERT_EQUALS(extb.getOp(), ext);
@@ -189,7 +189,7 @@ void TermBlack::testGetOp()
   TS_ASSERT(!f.hasOp());
   TS_ASSERT_THROWS(f.getOp(), CVC4ApiException&);
   TS_ASSERT(fx.hasOp());
-  TS_ASSERT_EQUALS(fx.getOp(), APPLY_UF);
+  TS_ASSERT_EQUALS(fx.getOp(), Op(&d_solver, APPLY_UF));
   std::vector<Term> children(fx.begin(), fx.end());
   // testing rebuild from op and children
   TS_ASSERT_EQUALS(fx, d_solver.mkTerm(fx.getOp(), children));
@@ -225,10 +225,10 @@ void TermBlack::testGetOp()
   TS_ASSERT(headTerm.hasOp());
   TS_ASSERT(tailTerm.hasOp());
 
-  TS_ASSERT_EQUALS(nilTerm.getOp(), APPLY_CONSTRUCTOR);
-  TS_ASSERT_EQUALS(consTerm.getOp(), APPLY_CONSTRUCTOR);
-  TS_ASSERT_EQUALS(headTerm.getOp(), APPLY_SELECTOR);
-  TS_ASSERT_EQUALS(tailTerm.getOp(), APPLY_SELECTOR);
+  TS_ASSERT_EQUALS(nilTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
+  TS_ASSERT_EQUALS(consTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
+  TS_ASSERT_EQUALS(headTerm.getOp(), Op(&d_solver, APPLY_SELECTOR));
+  TS_ASSERT_EQUALS(tailTerm.getOp(), Op(&d_solver, APPLY_SELECTOR));
 
   // Test rebuilding
   children.clear();