Add simple test suite for bounded unfolding

epfl-lara · Nov 22, 2019 · a15660e · a15660e
1 parent f2bea54
commit a15660e
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 2 deletions.
diff --git a/.larabot.conf b/.larabot.conf
@@ -1,6 +1,5 @@
 commands = [
-    "sbt -batch -Dparallel=5 test"
-    "sbt -batch -Dparallel=5 it:test"
+    "sbt -batch -Dparallel=1 it:testOnly *SMTZ3Unroll*"
 ]
 
 nightly {

diff --git a/frontends/scalac/src/it/scala/stainless/verification/VerificationSuite.scala b/frontends/scalac/src/it/scala/stainless/verification/VerificationSuite.scala
@@ -64,6 +64,20 @@ class SMTZ3VerificationSuite extends VerificationSuite {
   }
 }
 
+class SMTZ3UnrollBoundVerificationSuite(unrollBound: Int, unrollFactor: Int) extends SMTZ3VerificationSuite {
+  override def configurations = super.configurations.map {
+    seq => Seq(
+      inox.solvers.unrolling.optUnrollBound(unrollBound),
+      inox.solvers.unrolling.optUnrollFactor(unrollFactor),
+    ) ++ seq
+  }
+}
+
+class SMTZ3UnrollBoundOneOneSuite extends SMTZ3UnrollBoundVerificationSuite(1, 1)
+class SMTZ3UnrollBoundOneTwoSuite extends SMTZ3UnrollBoundVerificationSuite(1, 2)
+class SMTZ3UnrollBoundTwoOneSuite extends SMTZ3UnrollBoundVerificationSuite(2, 1)
+class SMTZ3UnrollBoundTwoTwoSuite extends SMTZ3UnrollBoundVerificationSuite(2, 2)
+
 class CodeGenVerificationSuite extends SMTZ3VerificationSuite {
   override def configurations = super.configurations.map {
     seq => Seq(