New C++ API: Add missing getType() calls to kick off type checking. (#2773)

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index d9a395d156dd07fd11b505b4368b177eec9e4be4..f9dfaa143571030f0f89e9d801cf891c3d7521e4 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1035,7 +1035,9 @@ Term Term::notTerm() const
 {
   try
   {
-    return d_expr->notExpr();
+    Term res = d_expr->notExpr();
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
   }
   catch (const CVC4::TypeCheckingException& e)
   {
@@ -1047,7 +1049,9 @@ Term Term::andTerm(const Term& t) const
 {
   try
   {
-    return d_expr->andExpr(*t.d_expr);
+    Term res = d_expr->andExpr(*t.d_expr);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
   }
   catch (const CVC4::TypeCheckingException& e)
   {
@@ -1059,7 +1063,9 @@ Term Term::orTerm(const Term& t) const
 {
   try
   {
-    return d_expr->orExpr(*t.d_expr);
+    Term res = d_expr->orExpr(*t.d_expr);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
   }
   catch (const CVC4::TypeCheckingException& e)
   {
@@ -1071,7 +1077,9 @@ Term Term::xorTerm(const Term& t) const
 {
   try
   {
-    return d_expr->xorExpr(*t.d_expr);
+    Term res = d_expr->xorExpr(*t.d_expr);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
   }
   catch (const CVC4::TypeCheckingException& e)
   {
@@ -1083,7 +1091,9 @@ Term Term::eqTerm(const Term& t) const
 {
   try
   {
-    return d_expr->eqExpr(*t.d_expr);
+    Term res = d_expr->eqExpr(*t.d_expr);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
   }
   catch (const CVC4::TypeCheckingException& e)
   {
@@ -1095,7 +1105,9 @@ Term Term::impTerm(const Term& t) const
 {
   try
   {
-    return d_expr->impExpr(*t.d_expr);
+    Term res = d_expr->impExpr(*t.d_expr);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
   }
   catch (const CVC4::TypeCheckingException& e)
   {
@@ -1107,7 +1119,9 @@ Term Term::iteTerm(const Term& then_t, const Term& else_t) const
 {
   try
   {
-    return d_expr->iteExpr(*then_t.d_expr, *else_t.d_expr);
+    Term res = d_expr->iteExpr(*then_t.d_expr, *else_t.d_expr);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
   }
   catch (const CVC4::TypeCheckingException& e)
   {

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 40f641cbdf5b4d4f61f1369cb0428eaae5d85bbb..5c2c7a8f5815eea3ae0f2f50b13f2ddca0a2b0b1 100644 (file)
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -288,7 +288,8 @@ void SolverBlack::testMkConst()
 
   // mkConst(Kind kind, Sort arg) const
   TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(EMPTYSET, Sort()));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(UNIVERSE_SET, d_solver.mkSetSort(d_solver.getBooleanSort())));
+  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(
+      UNIVERSE_SET, d_solver.mkSetSort(d_solver.getBooleanSort())));
   TS_ASSERT_THROWS(d_solver.mkConst(EMPTYSET, d_solver.getBooleanSort()),
                    CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver.mkTerm(UNIVERSE_SET, Sort()), CVC4ApiException&);