application.conf

// Suppress logging info
logger = ERROR

standard-timeout = 5 seconds

enabled = ["Z3"]

enabled = ${?ENABLED_SOLVERS}

app: [

  {
    name = "Z3"
    executable = "z3"
    version = "4.5.0"
    args = ["-in", "-smt2"]
    timeout = ${standard-timeout}
    interpolantCmd = get-interpolant
    prompt1 = "(\\\\s)*"
    prompt2 = ""
    supportedLogics = [QF_UF, QF_LIA, QF_LRA, AUFNIRA, QF_AUFLIA, QF_BV, QF_ABV, AUFNIRA, QF_AUFLIRA, QF_FPBV]
    supportedOptions = [PROOFS, MODELS, INTERPOLANTS]
    linux-distrib = "https://github.com/Z3Prover/z3/releases/download/z3-4.5.0/z3-4.5.0-x64-ubuntu-16.04.zip"
    macos-distrib = "https://github.com/Z3Prover/z3/releases/download/z3-4.5.0/z3-4.5.0-x64-osx-10.11.6.zip"
  },

  {
    name = "CVC4"
    executable = "cvc4"
    version = "1.4"
    args = ["--lang", "smt2", "-q", "--incremental"]
    timeout = ${standard-timeout}
    prompt1 = "(\\s)*\""
    prompt2 = "\"(\\s)*(success)"
    supportedLogics = [QF_UF, QF_LIA, QF_LRA, QF_AUFLIA, QF_BV, QF_ABV, QF_AUFLIRA, AUFNIRA]
    supportedOptions = [PROOFS, MODELS]
    linux-distrib = "http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.4-x86_64-linux-opt"
    macos-distrib = "http://cvc4.cs.stanford.edu/downloads/builds/macos/unstable/cvc4-devel-2017-01-05.MacOs85.MountainLion.mpkg"
  }

]