solver test tweak

apalache-mc · Oct 19, 2023 · d5312f8 · d5312f8
1 parent c857f3d
commit d5312f8
Showing 1 changed file with 19 additions and 17 deletions.
diff --git a/...forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestUninterpretedConstOracle.scala b/...forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestUninterpretedConstOracle.scala
@@ -135,24 +135,26 @@ class TestUninterpretedConstOracle extends AnyFunSuite with BeforeAndAfterEach w
     val ctx = new Z3SolverContext(SolverConfig.default)
     val paa = PureArenaAdapter.create(ctx) // We use PAA, since it performs the basic context initialization
     initScope = initScope.copy(arena = paa.arena)
-    val prop =
-      forAll(maxSizeAndIndexGen) { case (size, index) =>
-        cache.dispose() // prevent redeclarations in every loop
-        val (scope, oracle) = UninterpretedConstOracle.create(rewriter, cache, initScope, size)
-        ctx.push()
-        oracle.valueCells.foreach(ctx.declareCell)
-        ctx.declareCell(oracle.oracleCell)
-        cache.addAllConstraints(ctx)
-        val eql = oracle.chosenValueIsEqualToIndexedValue(scope, index)
-        ctx.assertGroundExpr(eql)
-        ctx.sat()
-        val ret = oracle.getIndexOfChosenValueFromModel(ctx) == index
-        ctx.pop()
-        ret
-      }
 
-    // 1000 is too many, since each run invokes the solver
-    check(prop, minSuccessful(80), sizeRange(4))
+    // We force this to be exhaustive, and non-parallelizable, because of strange interplay between the solver
+    // and scalatest `check`
+    for {
+      size <- 1 to 10
+      index <- 0 until size
+    } yield {
+      cache.dispose() // prevent redeclarations in every loop
+      val (scope, oracle) = UninterpretedConstOracle.create(rewriter, cache, initScope, size)
+      ctx.push()
+      oracle.valueCells.foreach(ctx.declareCell)
+      ctx.declareCell(oracle.oracleCell)
+      cache.addAllConstraints(ctx)
+      val eql = oracle.chosenValueIsEqualToIndexedValue(scope, index)
+      ctx.assertGroundExpr(eql)
+      ctx.sat()
+      val ret = oracle.getIndexOfChosenValueFromModel(ctx) == index
+      ctx.pop()
+      assert(ret)
+    }
   }
 
   test("getIndexOfChosenValueFromModel recovers the index correctly for empty collections") {