From a791ddb82699ce2e79167cbd974d48f3544549a1 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 13 Oct 2015 14:51:58 +0200
Subject: [PATCH] XLangVerificationSuite checks for z3
---
.../verification/XLangVerificationSuite.scala | 26 +++++++++++++++----
1 file changed, 21 insertions(+), 5 deletions(-)
diff --git a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
index 834597e79..3a9783e70 100644
--- a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
@@ -2,13 +2,29 @@
package leon.regression.verification
+import smtlib.interpreters.Z3Interpreter
+
class XLangVerificationSuite extends VerificationSuite {
- val optionVariants: List[List[String]] = List(
- List(),
- List("--feelinglucky"),
- List("--solvers=smt-z3", "--feelinglucky")
- )
+ val optionVariants: List[List[String]] = {
+ val isZ3Available = try {
+ Z3Interpreter.buildDefault.free()
+ true
+ } catch {
+ case e: java.io.IOException =>
+ false
+ }
+
+ List(
+ List(),
+ List("--feelinglucky")
+ ) ++ (
+ if (isZ3Available)
+ List(List("--solvers=smt-z3", "--feelinglucky"))
+ else Nil
+ )
+ }
+
val testDir: String = "regression/verification/xlang/"
override val desugarXLang = true
}
--
GitLab