From ff27591fd2b8999c8ef88940269e4d82d9b03b83 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Mon, 7 Nov 2016 15:26:22 +0100
Subject: [PATCH] Ignore tests where solvers aren't supported
---
src/it/scala/inox/TestSuite.scala | 10 +++++++++-
1 file changed, 9 insertions(+), 1 deletion(-)
diff --git a/src/it/scala/inox/TestSuite.scala b/src/it/scala/inox/TestSuite.scala
index 229e55c40..a227ad00e 100644
--- a/src/it/scala/inox/TestSuite.scala
+++ b/src/it/scala/inox/TestSuite.scala
@@ -27,7 +27,15 @@ trait TestSuite extends FunSuite with Matchers with Timeouts {
val ctx = Context(reporter, new InterruptManager(reporter), Options(config))
try {
val index = counter.nextGlobal
- super.test(f"$index%3d: $name ${optionsString(ctx.options)}")(body(ctx))
+ if (ctx.options.findOptionOrDefault(optSelectedSolvers).exists { sname =>
+ (sname == "nativez3" || sname == "unrollz3") && !solvers.SolverFactory.hasNativeZ3 ||
+ sname == "smt-z3" && !solvers.SolverFactory.hasZ3 ||
+ sname == "smt-cvc4" && !solvers.SolverFactory.hasCVC4
+ }) {
+ super.ignore(f"$index%3d: $name ${optionsString(ctx.options)}")(())
+ } else {
+ super.test(f"$index%3d: $name ${optionsString(ctx.options)}")(body(ctx))
+ }
} catch {
case err: FatalError =>
reporter.lastErrors :+= err.msg
--
GitLab