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?
