SMT-LIB Format

Here is the official SMT-LIB page.

To check satisfiability of formula

   (x = 2 \land x < y \land y < 0) \lor (x = y \land x < 3 \land 4 < y)

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$.