Merge pull request #254 from uclid-org/fix-253

Fix data type hashing; fix 253

Author: FedericoAureliano

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

src/test/scala/SMTLIB2Spec.scala

@@ -445,14 +445,15 @@ class SMTLIB2Spec extends AnyFlatSpec {
   "issue-187b.ucl" should "verify all assertions." in {
     SMTLIB2Spec.expectedFails("./test/issue-187b.ucl", 0)
   }
+  "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)
   }
   "test-redundant-assign.ucl" should "verify all assertions." in {
     SMTLIB2Spec.expectedFails("./test/test-redundant-assign.ucl", 0)
   }
-
-
   "test-history-1.ucl" should "verify all assertions." in {
     SMTLIB2Spec.expectedFails("./test/test-history-1.ucl", 0)
   }

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;
+    }
+}