chore(specs): Fix new errors yielded by latest Quint version (#228)

informalsystems · Jun 9, 2024 · c610128 · c610128
1 parent 3131656
commit c610128
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/specs/quint/specs/reset.qnt b/specs/quint/specs/reset.qnt
@@ -535,7 +535,7 @@ action addL1Block = all {
     nondet someHeight = (-1).to(L2.length() - 1).oneOf() 
     nondet blocktimeDelta = 1.to(MaxEthBlockTime).oneOf()
     val newproof = makeProof(L2, someHeight, L1)    // if someheight < provenHeight this will give Invalid proof
-    val submProof = Set(newproof, None).oneOf()
+    nondet submProof = Set(newproof, None).oneOf()
     L1' = L1.append(newL1Block(L1.last(), envRegs, submProof, blocktimeDelta)),
     L2' = L2,
     envRegs' = Set(),

diff --git a/specs/quint/tests/consensus/consensusTest.qnt b/specs/quint/tests/consensus/consensusTest.qnt
@@ -31,8 +31,8 @@ module consensusTest {
         }
 
     action step =
-        nondet h = 1 //oneOf(1.to(4))
-        nondet r = 0 //oneOf(1.to(4))
+        nondet h = oneOf(1.to(4))
+        nondet r = oneOf(1.to(4))
         nondet v = oneOf(Set("A", "B", "C"))
         nondet vr = oneOf(Set(-1, 1, 2, 3, 4))
         any {