How to build Z3 for Linux (for non-roots)

Now, suppose you are a normal user without root and you would like to run Z3 on Linux. How should you go about it? This blog posts documents what worked for me and I hope it will for you, too.

Set up a place for Z3 to be downloaded and built:

cd ~  # change to home folder
mkdir repositories  # create a folder called "repositories"
cd repositories  # go there

Once we are there, we can basically follow the readme instructions:

git clone https://git01.codeplex.com/z3  # downloads z3 source code
autoconf
./configure
python scripts/mk_make.py
cd build
make

The last step is setting execute permissions on Z3:

chmod 751 z3

That's it! Now you can run Z3 from this path. Try it now:

~/repositories/z3/build/z3 -version

Verifiying proofs with Z3

The Z3 theorem prover has a command for constructing proofs: (get-proof). The resulting files are not meant "for human consumption" and you can probably see why:

unsat
((set-logic <null>)
(proof
(let ((@x41 (monotonicity (rewrite (= (<= 2 a) (>= a 2))) (= (not (<= 2 a)) (not (>= a 2))))))
(let (($x19 (<= 2 a)))
(let (($x20 (not $x19)))
(let ((@x26 (monotonicity (rewrite (= $x19 $x19)) (= $x20 $x20))))
(let ((@x27 (trans (rewrite (= (< a 2) $x20)) @x26 (= (< a 2) $x20))))
(let (($x7 (< a 2)))
(let ((@x29 (mp (mp (|and-elim| (asserted (and (> a 3) $x7)) $x7) @x27 $x20) @x26 $x20)))
(let ((@x42 (mp (mp (mp @x29 (|rewrite*| (= $x20 $x20)) $x20) @x26 $x20) @x41 (not (>= a 2)))))
(let (($x39 (>= a 2)))
(let (($x15 (not (<= a 3))))
(let ((@x18 (mp (|and-elim| (asserted (and (> a 3) $x7)) (> a 3)) (rewrite (= (> a 3) $x15)) $x15)))
(let ((@x64 (|unit-resolution| ((_ |th-lemma| arith farkas 1 1) (or $x39 (<= a 3))) (mp @x18 (|rewrite*| (= $x15 $x15)) $x15) $x39)))
(|unit-resolution| @x64 @x42 false)))))))))))))))

Looking good, right? Well, hardly.
Even with nicer formatting, line breaks, etc. the proof is not quite readable. Now, it looks like people have actually managed to work with these proofs and I'm quite curious about how they accomplished that. There is a description of all the symbols used in the proof, but what I'm lacking is some kind of command line parameter which simply feeds the proof back into Z3.

If I ever find one (or build one), I'll write down here.