test.smt

;; activate interpolation
(set-option :produce-interpolants true)
(set-logic QF_LIA)

(declare-sort U 0)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)

(define-fun A1 () Bool (= y (* 2 x)))
(define-fun A2 () Bool (= y (+ (* 2 z) 1)))

;; use annotation :interpolation-group to partition the input problem into
;; several groups
(assert (! A1 :interpolation-group g1))
(assert (! A2 :interpolation-group g2))

(check-sat)

;; compute an interpolant for the given partition: the argument to
;; get-interpolant is a list of groups forming the A-part of the interpolation
;; problem
(get-interpolant (g1))

(exit)