Forcing a type check on Node construction in debug mode (Fixes: #188)

NOTE: mkNode/mkExpr/parsing functions can now throw type checking exceptions

1 files changed, 7 insertions, 1 deletions

diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 33e4c942f..354bf02bd 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -25,6 +25,8 @@
 #include "expr/type_node.h"
 #include "expr/expr.h"
 
+#include <sstream>
+
 namespace CVC4 {
 namespace theory {
 namespace builtin {
@@ -39,7 +41,11 @@ class EqualityTypeRule {
       TypeNode rhsType = n[1].getType(check);
 
       if ( lhsType != rhsType ) {
-        throw TypeCheckingExceptionPrivate(n, "Left and right hand side of the equation are not of the same type");
+        std::stringstream ss;
+        ss << "Types do not match in equation ";
+        ss << "[" << lhsType << "<>" << rhsType << "]";
+        
+        throw TypeCheckingExceptionPrivate(n, ss.str());
       }
 
       if ( lhsType == booleanType ) {