From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 7 Oct 2014 01:22:57 +0000 (-0400)
Subject: Some minor cleanup.
X-Git-Tag: cvc5-1.0.0~6588
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1c494313662b664a606f6f745f67cbd964c61927;p=cvc5.git

Some minor cleanup.
---

diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h
index d2836c85e..9d12e1bb1 100644
--- 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 */