(set-logic QF_LIA)
(set-option :produce-models true)
(declare-const a1 Int)
(declare-const a2 Int)
(declare-const b1 Int)
(declare-const b2 Int)

(assert (and (>= a1 0) (>= a2 0)
             (>= b1 0) (>= b2 0)))

; Each order must be milled before it is painted.
(assert (<= (+ a1 3) a2))
(assert (<= (+ b1 2) b2))

; The milling machine handles at most one operation at a time.
(assert (or (<= (+ a1 3) b1)
            (<= (+ b1 2) a1)))

; The painting booth has the same capacity constraint.
(assert (or (<= (+ a2 2) b2)
            (<= (+ b2 3) a2)))

; Test a deadline without permanently asserting it.
(push 1)
(assert (and (<= (+ a2 2) 7) (<= (+ b2 3) 7)))
(check-sat)                 ; sat
(get-value (a1 a2 b1 b2))   ; a1=2, a2=5, b1=0, b2=2
(pop 1)

(push 1)
(assert (and (<= (+ a2 2) 6) (<= (+ b2 3) 6)))
(check-sat)                 ; unsat
(pop 1)
(exit)