Is the DPLL(T)-style SMT solving in z3 documented for Linear Real Arithmetic?

Question

I am trying to devise ways to improve performance of z3 on my problems. I am aware of the the CAV'06 paper and the tech report . Do relevant parts of z3 v4.3.1 differ from what is described in these documents, and if so in what ways? Also, what is the strategy followed by default in z3 for deciding when to check for consistency in Linear Real Arithmetic, of the theory atoms corresponding to the decided (and propagated) propositional literals?

Answer 1

Linear arithmetic is implemented in the files at src/smt/theory_arith*. See http://z3.codeplex.com/SourceControl/latest#src/smt/theory_arith_core.h

Regarding the paper you pointed out, the ideas are used in the implementation. However, the actual code contains many extensions for linear integer, nonlinear arithmetic and proof generation. If you only care about linear real arithmetic, you should focus only on theory_arith.h, theory_arith_core.h. The file theory_arith_aux.h also contains useful functionality.