From 1f6fb54967659ff2ee3f8c29a8d306499fcf1299 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Mon, 7 Jan 2019 09:02:02 -0800
Subject: [PATCH] New C++ API: Add missing getType() calls to kick off type
 checking. (#2773)

---
 src/api/cvc4cpp.cpp          | 28 +++++++++++++++++++++-------
 test/unit/api/solver_black.h |  3 ++-
 2 files changed, 23 insertions(+), 8 deletions(-)

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index d9a395d15..f9dfaa143 100644
--- 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 40f641cbd..5c2c7a8f5 100644
--- 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&);
-- 
2.30.2