add test to CI and remove control block to avoid needless solver call

uclid-org · Jul 17, 2024 · f4fae77 · f4fae77
1 parent 601752b
commit f4fae77
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 6 deletions.
diff --git a/src/test/scala/ParserSpec.scala b/src/test/scala/ParserSpec.scala
@@ -206,6 +206,11 @@ class ParserSpec extends AnyFlatSpec {
         assert (p.errors.size > 0)
     }
   }
+  "test-record-rename.ucl" should "parse successfully" in {
+    val fileModules = UclidMain.compile(ConfigCons.createConfig("test/test-record-rename.ucl"), lang.Identifier("main"))
+    val instantiatedModules = UclidMain.instantiateModules(UclidMain.Config(), fileModules, lang.Identifier("main"))
+    assert (instantiatedModules.size == 1)
+  }
   "test-type1.ucl" should "not parse successfully." in {
     try {
       val filename = "test/test-type1.ucl"

diff --git a/test/test-record-rename.ucl b/test/test-record-rename.ucl
@@ -4,10 +4,4 @@ module main {
     init {
         assert forall (x: r) :: x.y > 0;
     }
-
-    control {
-        unroll(0);
-        check;
-        print_results;
-    }
 }