diff options
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 8 |
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 ) { |