LARA

SMT-LIB Format

Here is the official SMT-LIB page.

To check satisfiability of formula

\begin{equation*} (x = 2 \land x < y \land y < 0) \lor (x = y \land x < 3 \land 4 < y) \end{equation*}

you can write the following file in SMT-LIB format: 

(benchmark test
  :extrafuns ((x Int) (y Int))

  :formula (or (and (= x 2) (< x y) (< y 0))
  	       (and (= x y) (< x 3) (< 4 y)))
)

Here is the Web site for CVC3 prover, with documentation and download.

To invoke CVC3 on file test.smt file in SMT-LIB format, use command line 

cvc3 -lang smt test.smt

The prover should output “sat” or “unsat” on the standard output.

Formula $F$ is valid if the prover outpus “unsat” on a file encoding formula $\lnot F$.