diff --git a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala index 834597e79adce7675e1190359aee34e864ccf37f..3a9783e7036ca82d51298b6eb1751e5ee024d46a 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 }