DPLL(T) algorithm used in Z3 (linear arithmetic)

Question

The arithmetic solver of Z3 is developed based on DPLL(T) and Simplex (described in this paper). And I do not understand how Z3 perform the backtrack when a conflict explanation is generated. I give an example:

The linear arithmetic formula is:

(2x1+x2≤200 OR 3x1+x2≤250) AND (2x1+x2+x3≤200 OR 4x1+2x2+x3≤400) AND x1≥50 AND x2≥50 AND x3≥60

after asserting 2x1+x2≤200, 2x1+x2+x3≤200, x1≥50, x2≥50 and x3≥60 successively, it yields a conflict explanation set {2x1+x2+x3≤200, x1≥50, x2≥50, x3≥60}.

My question is, how then the backtrack is performed when this conflict set is generated?

Answer 1

The main paper to read for understanding the algorithm is:

 A Fast Linear-Arithmetic Solver for DPLL(T)
 Bruno Dutertre,  Leonardo de Moura 

Download: .pdf