From dc0dc0b91f3d3359dd0b301fdabcd3fd8b035b4a Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Wed, 4 Dec 2024 11:35:24 +0100 Subject: [PATCH 1/2] fail silently solvers by default --- src/main/scala/inox/solvers/Solver.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/inox/solvers/Solver.scala b/src/main/scala/inox/solvers/Solver.scala index b28f85d0a..e5cfb5b87 100644 --- a/src/main/scala/inox/solvers/Solver.scala +++ b/src/main/scala/inox/solvers/Solver.scala @@ -7,7 +7,7 @@ import utils._ object optCheckModels extends FlagOptionDef("check-models", false) object optIgnoreModels extends FlagOptionDef("ignore-models", false) -object optSilentErrors extends FlagOptionDef("silent-errors", false) +object optSilentErrors extends FlagOptionDef("silent-errors", true) case object DebugSectionSolver extends DebugSection("solver") From dc8e6747e05fa529faa7096d97bd6f9dfed58499 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Wed, 4 Dec 2024 13:53:26 +0100 Subject: [PATCH 2/2] pass option in tests to not fail silently --- src/it/scala/inox/tip/TipTestSuite.scala | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/it/scala/inox/tip/TipTestSuite.scala b/src/it/scala/inox/tip/TipTestSuite.scala index c23e619ea..ff671b84d 100644 --- a/src/it/scala/inox/tip/TipTestSuite.scala +++ b/src/it/scala/inox/tip/TipTestSuite.scala @@ -10,11 +10,11 @@ import scala.language.existentials class TipTestSuite extends TestSuite with ResourceUtils { override def configurations = Seq( - Seq(optSelectedSolvers(Set("nativez3")), optCheckModels(true)), - Seq(optSelectedSolvers(Set("smt-z3")), optCheckModels(true)), - Seq(optSelectedSolvers(Set("smt-cvc4")), optCheckModels(true)), - Seq(optSelectedSolvers(Set("smt-z3")), optCheckModels(true), optAssumeChecked(true)), - Seq(optSelectedSolvers(Set("no-inc:smt-z3")), optCheckModels(true)) + Seq(optSelectedSolvers(Set("nativez3")), optSilentErrors(false), optCheckModels(true)), + Seq(optSelectedSolvers(Set("smt-z3")), optSilentErrors(false), optCheckModels(true)), + Seq(optSelectedSolvers(Set("smt-cvc4")), optSilentErrors(false), optCheckModels(true)), + Seq(optSelectedSolvers(Set("smt-z3")), optSilentErrors(false), optCheckModels(true), optAssumeChecked(true)), + Seq(optSelectedSolvers(Set("no-inc:smt-z3")), optSilentErrors(false), optCheckModels(true)) ) override protected def optionsString(options: Options): String = {