From a15660e1e4752698811adea7f3e7b9a13e86a3fb Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Fri, 22 Nov 2019 16:04:32 +0100 Subject: [PATCH] Add simple test suite for bounded unfolding --- .larabot.conf | 3 +-- .../stainless/verification/VerificationSuite.scala | 14 ++++++++++++++ 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/.larabot.conf b/.larabot.conf index ce806393f8..bd70e1e6e9 100644 --- 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 index 1940aa3994..652c92398e 100644 --- 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(