From 512a640398b3559421ece8931f413169d01d35ee Mon Sep 17 00:00:00 2001
From: FedericoAureliano <fmorarocha@gmail.com>
Date: Wed, 3 Jul 2024 21:55:54 -0700
Subject: [PATCH] fix data type hashing

---
 src/main/scala/uclid/smt/SMTLanguage.scala |  4 ++--
 test/issue-253.ucl                         | 19 +++++++++++++++++++
 2 files changed, 21 insertions(+), 2 deletions(-)
 create mode 100644 test/issue-253.ucl

diff --git a/src/main/scala/uclid/smt/SMTLanguage.scala b/src/main/scala/uclid/smt/SMTLanguage.scala
index 8b070ffc..e1195e56 100644
--- a/src/main/scala/uclid/smt/SMTLanguage.scala
+++ b/src/main/scala/uclid/smt/SMTLanguage.scala
@@ -201,8 +201,8 @@ case object UndefinedType extends Type {
 
 case class DataType(id : String, cstors : List[ConstructorType]) extends Type {
   override val hashId = 111
-  override val hashCode = finalize(hashId, 0)
-  override val md5hashCode = computeMD5Hash
+  override val hashCode = computeHash(id, cstors)
+  override val md5hashCode = computeMD5Hash(id, cstors)
   override def toString = "data " + cstors // TODO
   override val typeNamePrefix = "data"
   override def isUndefined = true
diff --git a/test/issue-253.ucl b/test/issue-253.ucl
new file mode 100644
index 00000000..ea08a51c
--- /dev/null
+++ b/test/issue-253.ucl
@@ -0,0 +1,19 @@
+module main {
+    datatype adt1 = A() | B();
+    datatype adt2 = C() | D();
+
+    var y: adt1;
+    var x: adt2;
+
+    init {
+        assert y == B();
+        assert x == C();
+    }
+
+
+    control {
+        bmc(0);
+        check;
+        print_results;
+    }
+}
\ No newline at end of file