Skip to content
Snippets Groups Projects
  • Etienne Kneuss's avatar
    20e8c86a
    Refactor tests, again. · 20e8c86a
    Etienne Kneuss authored
    unit, integration, and regression tests can now share code as they are
    compiled together.
    
    Unit tests are now in package leon.unit and shared code lives in
    leon.test.
    20e8c86a
    History
    Refactor tests, again.
    Etienne Kneuss authored
    unit, integration, and regression tests can now share code as they are
    compiled together.
    
    Unit tests are now in package leon.unit and shared code lives in
    leon.test.
PureScalaVerificationSuite.scala 1.29 KiB
/* Copyright 2009-2015 EPFL, Lausanne */

package leon.regression
package verification

import leon._
import leon.verification.AnalysisPhase

import _root_.smtlib.interpreters._

// If you add another regression test, make sure it contains one object whose name matches the file name
// This is because we compile all tests from each folder separately.
class PureScalaVerificationSuite extends VerificationSuite {
  
  val testDir = "regression/verification/purescala/"
  val pipeFront = xlang.NoXLangFeaturesChecking
  val pipeBack = AnalysisPhase
  val optionVariants: List[List[String]] = {
    val isZ3Available = try {
      Z3Interpreter.buildDefault.free()
      true
    } catch {
      case e: java.io.IOException =>
        false
    }

    val isCVC4Available = try {
      CVC4Interpreter.buildDefault.free()
      true
    } catch {
      case e: java.io.IOException =>
        false
    }

    List(
      List("--feelinglucky"),
      List("--codegen", "--evalground", "--feelinglucky"),
      List("--solvers=fairz3,enum", "--codegen", "--evalground", "--feelinglucky")
    ) ++ (
      if (isZ3Available) List(
        List("--solvers=smt-z3", "--feelinglucky")
      ) else Nil
    ) ++ (
      if (isCVC4Available) List(
        List("--solvers=smt-cvc4", "--feelinglucky")
      ) else Nil
    )
  }

}