Some minor cleanup.

diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h
index d2836c85e802baa301145d8890bcf83d32e2e118..9d12e1bb1e69877d4080bc3bec5660360e827a14 100644 (file)
--- a/src/theory/booleans/theory_bool_type_rules.h
+++ b/src/theory/booleans/theory_bool_type_rules.h
@@ -42,10 +42,10 @@ public:
     }
     return booleanType;
   }
-};
+};/* class BooleanTypeRule */
 
 class IteTypeRule {
-  public:
+public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     TypeNode thenType = n[1].getType(check);
@@ -57,15 +57,21 @@ class IteTypeRule {
         throw TypeCheckingExceptionPrivate(n, "condition of ITE is not Boolean");
       }
       if (iteType.isNull()) {
-        throw TypeCheckingExceptionPrivate(n, "both branches of the ITE must be a subtype of a common type.");
+        std::stringstream ss;
+        ss << "Both branches of the ITE must be a subtype of a common type." << std::endl
+           << "then branch: " << n[1] << std::endl
+           << "its type   : " << thenType << std::endl
+           << "else branch: " << n[2] << std::endl
+           << "its type   : " << elseType << std::endl;
+        throw TypeCheckingExceptionPrivate(n, ss.str());
       }
     }
     return iteType;
   }
-};
+};/* class IteTypeRule */
 
-}/* namespace CVC4::theory::boolean */
-}/* namespace CVC4::theory */
-}/* namespace CVC4 */
+}/* CVC4::theory::boolean namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
 #endif /* __CVC4__THEORY_BOOL_TYPE_RULES_H */