From 288ce349416c04b5b0dbd598dac4761e5a57aa42 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Mon, 17 Mar 2014 12:27:31 +0100
Subject: [PATCH] Fix Equality of Implies. Disambiguate other's hashCode a bit.

---
 src/main/scala/leon/purescala/Trees.scala | 24 ++++++++++-------------
 1 file changed, 10 insertions(+), 14 deletions(-)

diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 7ff43180b..877bc6a62 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -127,7 +127,7 @@ object Trees {
       case _ => false
     })
 
-    override def hashCode: Int = tuple.hashCode + index.hashCode
+    override def hashCode: Int = tuple.hashCode + index.hashCode + 1
   }
 
   object MatchExpr {
@@ -160,7 +160,7 @@ object Trees {
       case _ => false
     })
 
-    override def hashCode: Int = scrutinee.hashCode+cases.hashCode
+    override def hashCode: Int = scrutinee.hashCode + cases.hashCode + 2
   }
 
   sealed abstract class MatchCase extends Tree {
@@ -236,7 +236,7 @@ object Trees {
       case _ => false
     })
 
-    override def hashCode: Int = exprs.hashCode
+    override def hashCode: Int = exprs.hashCode + 3
   }
 
   object Or {
@@ -279,7 +279,7 @@ object Trees {
       case _ => false
     })
 
-    override def hashCode: Int = exprs.hashCode
+    override def hashCode: Int = exprs.hashCode + 4
   }
 
   object Iff {
@@ -304,7 +304,7 @@ object Trees {
       case _ => false
     })
 
-    override def hashCode: Int = left.hashCode + right.hashCode
+    override def hashCode: Int = left.hashCode + right.hashCode + 5
   }
 
   object Implies {
@@ -322,17 +322,13 @@ object Trees {
 
   class Implies(val left: Expr, val right: Expr) extends Expr with FixedType {
     val fixedType = BooleanType
-    // if(left.getType != BooleanType || right.getType != BooleanType) {
-    //   println("culprits: " + left.getType + ", " + right.getType)
-    //   assert(false)
-    // }
 
     override def equals(that: Any): Boolean = (that != null) && (that match {
-      case t: Iff => t.left == left
+      case t: Implies => t.left == left && t.right == right
       case _ => false
     })
 
-    override def hashCode: Int = left.hashCode + right.hashCode
+    override def hashCode: Int = left.hashCode + right.hashCode + 6
   }
 
   object Not {
@@ -355,7 +351,7 @@ object Trees {
       case _ => false
     })
 
-    override def hashCode : Int = expr.hashCode ^ Int.MinValue
+    override def hashCode : Int = expr.hashCode + 7
   }
 
   object Equals {
@@ -390,7 +386,7 @@ object Trees {
       case _ => false
     })
 
-    override def hashCode: Int = left.hashCode+right.hashCode
+    override def hashCode: Int = left.hashCode + right.hashCode + 8
   }
   
   case class Variable(id: Identifier) extends Expr with Terminal {
@@ -455,7 +451,7 @@ object Trees {
       case _ => false
     })
 
-    override def hashCode: Int = (classType, caseClass, selector).hashCode
+    override def hashCode: Int = (classType, caseClass, selector).hashCode + 9
   }
 
   /* Arithmetic */
-- 
GitLab