fix data type hashing

uclid-org · Jul 4, 2024 · 512a640 · 512a640
1 parent 6f3f8da
commit 512a640
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 2 deletions.
diff --git 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
@@ -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;
+    }
+}