Explanation of a tree interpolation query in Z3 4.6.0

[prantikchatterjee]

I am trying to use tree interpolation in Z3. It seems that this is no longer supported in the newer versions, however, I was able to run it on Z3 4.6.0, but the results are quite weird. For example, for the given SMT query, I get the following output:

(set-option :produce-models true)
(set-option :produce-interpolants true)
(set-logic ALL) ; has unbounded values, using catch-all.
(declare-fun x () Int)
(declare-fun x1 () Int)
(declare-fun x2 () Int)

(assert (! (and (> x 25) (= x x1 x2)) :named A))
(assert (! (< x1 30) :named B))
(assert (! (or (< x2 0) (> x2 35)) :named C))
(check-sat)
(get-interpolant A (interp B) (interp C))

output___________________

unsat
(interpolants
(or (and (<= x2 35) (>= x2 0)) (>= x1 30))
(not (>= x1 30))
(and (<= x2 35) (>= x2 0))
(or (not (>= x2 0)) (not (<= x2 35))))

I would have expected two interpolants, corresponding to the leaves, but it gives out four.

Am I making some mistake on the syntax?

[NikolajBjorner]

Sorry, there is no support for old versions of z3, functionality that was removed.
It is also unlikely that Ken McMillan is reading this thread so you are better off contacting him directly on questions.