From a2a571361979b542f7d759456d6219b3ca1f5e9b Mon Sep 17 00:00:00 2001 From: Nicolas Voirol <voirol.nicolas@gmail.com> Date: Fri, 21 Oct 2016 15:07:26 +0200 Subject: [PATCH] Updated tests for new options --- src/it/scala/inox/InoxTestSuite.scala | 2 +- src/it/scala/inox/solvers/SolvingTestSuite.scala | 4 ++-- .../inox/solvers/unrolling/AssociativeQuantifiersSuite.scala | 4 ++-- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/it/scala/inox/InoxTestSuite.scala b/src/it/scala/inox/InoxTestSuite.scala index 6ee309d99..d94fcca60 100644 --- a/src/it/scala/inox/InoxTestSuite.scala +++ b/src/it/scala/inox/InoxTestSuite.scala @@ -12,7 +12,7 @@ trait InoxTestSuite extends FunSuite with Matchers with Timeouts { val configurations: Seq[Seq[OptionValue[_]]] = Seq(Seq.empty) private def optionsString(options: Options): String = { - "solver=" + options.findOptionOrDefault(InoxOptions.optSelectedSolvers).head + " " + + "solver=" + options.findOptionOrDefault(optSelectedSolvers).head + " " + "feelinglucky=" + options.findOptionOrDefault(solvers.unrolling.optFeelingLucky) + " " + "checkmodels=" + options.findOptionOrDefault(solvers.optCheckModels) + " " + "unrollassumptions=" + options.findOptionOrDefault(solvers.unrolling.optUnrollAssumptions) diff --git a/src/it/scala/inox/solvers/SolvingTestSuite.scala b/src/it/scala/inox/solvers/SolvingTestSuite.scala index 7129c9fb7..17b9c8630 100644 --- a/src/it/scala/inox/solvers/SolvingTestSuite.scala +++ b/src/it/scala/inox/solvers/SolvingTestSuite.scala @@ -11,11 +11,11 @@ trait SolvingTestSuite extends InoxTestSuite { feelingLucky <- Seq(false, true) unrollAssumptions <- Seq(false, true) } yield Seq( - InoxOptions.optSelectedSolvers(Set(solverName)), + optSelectedSolvers(Set(solverName)), optCheckModels(checkModels), unrolling.optFeelingLucky(feelingLucky), unrolling.optUnrollAssumptions(unrollAssumptions), - InoxOptions.optTimeout(300), + optTimeout(300), ast.optPrintUniqueIds(true) ) } diff --git a/src/it/scala/inox/solvers/unrolling/AssociativeQuantifiersSuite.scala b/src/it/scala/inox/solvers/unrolling/AssociativeQuantifiersSuite.scala index 28be5f5ef..4ebc09cb9 100644 --- a/src/it/scala/inox/solvers/unrolling/AssociativeQuantifiersSuite.scala +++ b/src/it/scala/inox/solvers/unrolling/AssociativeQuantifiersSuite.scala @@ -16,11 +16,11 @@ class AssociativeQuantifiersSuite extends InoxTestSuite { ("nativez3", false, false, true ), ("smt-cvc4", false, false, true ) ).map { case (solverName, checkModels, feelingLucky, unrollAssumptions) => Seq( - InoxOptions.optSelectedSolvers(Set(solverName)), + optSelectedSolvers(Set(solverName)), optCheckModels(checkModels), optFeelingLucky(feelingLucky), optUnrollAssumptions(unrollAssumptions), - InoxOptions.optTimeout(300), + optTimeout(300), ast.optPrintUniqueIds(true) )} -- GitLab