(set-option :print-success false) (set-option :produce-proofs true) (set-logic QF_LIA) (declare-fun x () Int) (declare-fun y () Int) (assert (! (> x y) :named IP_0)) (assert (! (= x 0) :named IP_1)) (assert (! (> y 0) :named IP_2)) (check-sat) (get-interpolants IP_0 IP_1 IP_2) (get-interpolants IP_1 (and IP_0 IP_2)) (exit)