(set-logic QF_LRA) (set-option :produce-interpolants true) (set-option :interpolation-lra-algorithm 0) (set-option :verbosity 2) (declare-fun x () Real) (declare-fun y () Real) (assert (or (and (<= x 1) (<= y 3) ) (and (<= 1 x) (<= x 2) (<= y 2) ) (and (<= 2 x) (<= x 3) (<= y 1) ) ) ) (assert (or (and (>= x 3) (>= y 4) ) (and (>= x 4) (<= 3 y) (<= y 4) ) ) ) (check-sat) (get-interpolants)