The Z3 SMT Solver

See http://z3.codeplex.com/.

Easy mode for Windows/Linux: http://www.fdi.ucm.es/profesor/fernan/ACIDE/html/z3.html
The specific distribution of Linux doesn't actually matter.
Literally just do that and skip everything else.

1. Installation

We will install z3 using stow, so first follow the instructions here.

cd ~/local/src
git clone https://github.com/Z3Prover/z3.git
cd z3
hash=$(git rev-parse --short HEAD)
pkg=z3-${hash}
./configure --prefix ~/local/stow/$pkg
cd build
make -j4
make install
cd ~/local/stow
stow $pkg

1.1. Editing

If you're using VIM, put this as the last line any file:

; vim: ft=lisp:lw+=define-fun,forall,exists:

Or do it properly by putting the following line in ~/.vim/filetype.vim:

autocmd BufRead,BufNewFile *.smt2 set ft=lisp lisp lw+=define-fun,forall,exists

2. Using It

Follow this interactive tutorial: http://rise4fun.com/Z3/tutorial/guide