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 1/4] 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

From 97540fe4140c5e2bc2094c744b2cc67f4ecc5b7d Mon Sep 17 00:00:00 2001
From: FedericoAureliano <fmorarocha@gmail.com>
Date: Wed, 3 Jul 2024 21:59:57 -0700
Subject: [PATCH 2/4] add test case to CI

---
 src/test/scala/SMTLIB2Spec.scala | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/test/scala/SMTLIB2Spec.scala b/src/test/scala/SMTLIB2Spec.scala
index 502fba63..14e17e62 100644
--- a/src/test/scala/SMTLIB2Spec.scala
+++ b/src/test/scala/SMTLIB2Spec.scala
@@ -445,6 +445,9 @@ class SMTLIB2Spec extends AnyFlatSpec {
   "issue-187b.ucl" should "verify all assertions." in {
     SMTLIB2Spec.expectedFails("./test/issue-187b.ucl", 0)
   }
+  "issue-253.ucl" should "verify all assertions." in {
+    SMTLIB2Spec.expectedFails("./test/issue-253.ucl", 0)
+  }
   "test-redundant-assign.ucl" should "verify all assertions." in {
     SMTLIB2Spec.expectedFails("./test/test-redundant-assign.ucl", 0)
   }

From cd2890331c105ca115b0184e174e247ffebf4a32 Mon Sep 17 00:00:00 2001
From: FedericoAureliano <fmorarocha@gmail.com>
Date: Wed, 3 Jul 2024 22:02:12 -0700
Subject: [PATCH 3/4] fix buggy test: we actually expect issue-253 to fail two
 assertions

---
 src/test/scala/SMTLIB2Spec.scala | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/test/scala/SMTLIB2Spec.scala b/src/test/scala/SMTLIB2Spec.scala
index 14e17e62..a90f343c 100644
--- a/src/test/scala/SMTLIB2Spec.scala
+++ b/src/test/scala/SMTLIB2Spec.scala
@@ -445,8 +445,8 @@ class SMTLIB2Spec extends AnyFlatSpec {
   "issue-187b.ucl" should "verify all assertions." in {
     SMTLIB2Spec.expectedFails("./test/issue-187b.ucl", 0)
   }
-  "issue-253.ucl" should "verify all assertions." in {
-    SMTLIB2Spec.expectedFails("./test/issue-253.ucl", 0)
+  "issue-253.ucl" should "fail all 2 assertions." in {
+    SMTLIB2Spec.expectedFails("./test/issue-253.ucl", 2)
   }
   "test-redundant-assign.ucl" should "verify all assertions." in {
     SMTLIB2Spec.expectedFails("./test/test-redundant-assign.ucl", 0)

From a063957f3475116a84ba16c49437937f0a6141f1 Mon Sep 17 00:00:00 2001
From: FedericoAureliano <fmorarocha@gmail.com>
Date: Wed, 17 Jul 2024 09:49:12 -0700
Subject: [PATCH 4/4] fix missing paren introduced by trying to use github's
 conflict resolution

---
 src/test/scala/SMTLIB2Spec.scala | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/test/scala/SMTLIB2Spec.scala b/src/test/scala/SMTLIB2Spec.scala
index 36f572ca..719a1b5f 100644
--- a/src/test/scala/SMTLIB2Spec.scala
+++ b/src/test/scala/SMTLIB2Spec.scala
@@ -447,6 +447,7 @@ class SMTLIB2Spec extends AnyFlatSpec {
   }
   "issue-253.ucl" should "fail all 2 assertions." in {
     SMTLIB2Spec.expectedFails("./test/issue-253.ucl", 2)
+  }
   "issue-255.ucl" should "faill single assertion." in {
     SMTLIB2Spec.expectedFails("./test/issue-255.ucl", 1)
   }