list of provers

• (prover
    (name z3)
    (version "")
    (cmd "z3 $file")
    (binary z3)
    (ulimit (time memory ))
    (sat "(^sat)|(s SATISFIABLE)")
    (unsat "unsat|(s UNSATISFIABLE)")
    (defined_in prelude)
    (produces_proof false))

  defined in prelude

• (prover
    (name smtlib-read-status)
    (version <unknown>)
    (cmd "grep :status $file")
    (binary grep)
    (ulimit (time memory ))
    (sat ":status sat")
    (unsat ":status unsat")
    (unknown ":status unknown")
    (defined_in prelude)
    (produces_proof false))

  defined in prelude

• (prover
    (name minisat)
    (version <unknown>)
    (cmd "minisat -cpu-lim=$timeout $file")
    (binary minisat)
    (ulimit (time memory ))
    (sat "^SATISFIABLE")
    (unsat "UNSATISFIABLE")
    (defined_in prelude)
    (produces_proof false))

  defined in prelude

• (prover
    (name cvc4)
    (version "")
    (cmd "cvc4 $file ")
    (binary cvc4)
    (ulimit (time memory ))
    (sat "^sat")
    (unsat "unsat")
    (defined_in prelude)
    (produces_proof false))

  defined in prelude