3 files changed, 5 insertions, 4 deletions
diff --git a/src/expr/builtin_type_rules.h b/src/expr/builtin_type_rules.h
index 2a6b43b22..e0ad0b038 100644
--- a/src/expr/builtin_type_rules.h
+++ b/src/expr/builtin_type_rules.h
@@ -23,7 +23,7 @@ namespace CVC4 {
 
 class EqualityTypeRule {
   public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n) throw (TypeCheckingException) {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n) throw (TypeCheckingExceptionPrivate) {
     if (n[0].getType() != n[1].getType()) {
       throw TypeCheckingExceptionPrivate(n, "Left and right hand side of the equation are not of the same type");
     }
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index da16000ce..821349b45 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -28,7 +28,8 @@ bool TypeNode::isInteger() const {
 }
 
 bool TypeNode::isReal() const {
-  return getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == REAL_TYPE;
+  return getKind() == kind::TYPE_CONSTANT
+    && (getConst<TypeConstant>() == REAL_TYPE || getConst<TypeConstant>() == INTEGER_TYPE);
 }
 
 /** Is this a function type? */
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 1d32fffda..f7b1a6b9e 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -110,7 +110,7 @@ public:
    * @return true if expressions are equal, false otherwise
    */
   bool operator==(const TypeNode& typeNode) const {
-    return d_nv == typeNode.d_nv;
+    return d_nv == typeNode.d_nv || (typeNode.isReal() && this->isReal());
   }
 
   /**
@@ -119,7 +119,7 @@ public:
    * @return true if expressions are equal, false otherwise
    */
   bool operator!=(const TypeNode& typeNode) const {
-    return d_nv != typeNode.d_nv;
+    return !(*this == typeNode);
   }
 
   /**