diff --git a/src/it/scala/inox/InoxTestSuite.scala b/src/it/scala/inox/InoxTestSuite.scala index 6ee309d99a3b0af7387dd073fdd3cd660b672711..d94fcca6009063943a9b2bc7682b9051029e9f2c 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 7129c9fb7b9a331e8d43e16eea1d25c91377a9b2..17b9c8630f0649b11972ee21abeba31e315dcee0 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 28be5f5ef206331d3b9a7072d64160be7fa1779f..4ebc09cb94215a38beaa8012bafde9346e880b8f 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) )}