This is an old revision of the document!
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 is valid if the prover outpus “unsat” on a file encoding formula .