Z3 Interpolants in presence of quantifiers

Question

I am experimenting with iZ3 to see if I can derive quantified invariants making use of iZ3's get-interpolant functionality. Here is my example:

(set-option :auto-config false)                                             
(set-option :smt.mbqi true)
(set-option :smt.macro-finder true)
(set-option :produce-interpolants true)                                         
(declare-sort T0)
(declare-const l1 T0)                                                       
(declare-const l2 T0)                                                       
(declare-const v T0)                                                        
(declare-sort T1)
(declare-const z1 T1)                                                       
(declare-const z2 T1)                                                       
(declare-const z3 T1)
(declare-fun Rmem (T0 T1) Bool)                                             
(declare-const phi1 Bool)                                                   
(declare-const phi2 Bool)                                                   
(declare-const assn1 Bool)
(declare-const assn2 Bool)
;; A fact: \forall x. (Rmem(l1) = {x}) => (Rmem(v) = {x} \union Rmem(l2))
(assert (! (= phi1 (forall ((x T1))
    (=> (forall ((bv0 T1)) (= (Rmem l1 bv0) (= bv0 x)))                     
        (forall ((bv0 T1)) (= (Rmem v bv0)
                           (or (Rmem l2 bv0) (= bv0 x))))))) :named f1))               
;; An observation: When (Rmem(l1) = {z1}) and (Rmem(l2)= {z2,z3}), then
;;                 Rmem(v) was observed to be {z1,z2,z3}
(assert (! (= phi2 (! (=> (and (forall ((bv0 T1))
                            (= (Rmem l1 bv0) (= bv0 z1)))                   
                         (forall ((bv0 T1))
                            (= (Rmem l2 bv0) (or (= bv0 z2) (= bv0 z3)))))  
                    (forall ((bv0 T1))
                        (= (Rmem v bv0) (or (= bv0 z1) (= bv0 z2)           
                                            (= bv0 z3))))))) :named f2))
(assert (= assn2 (and phi1 (not phi2))))
(assert assn2)                                      
(check-sat)                                                                 
;; Can Z3 derive the following invariant: Rmem(v) = Rmem(l1) \union Rmem(l2)?
(get-interpolant f1 f2)

For the above example, Z3 prints Unsat (as expected), but nothing else.

1. Does this mean that Z3 was unable to derive interpolants from the proof of unsatisfiability?
2. I understand that iZ3 has limited support for quantifiers. Notwithstanding, I expected interpolation to succeed because my example is in decidable (EPR) logic. Is the failure due to inherent limitations of Z3? If not, are there any alternative ways constructing my query?

Answer 1

I get this result for your file:

unsat
(forall ((%0 T1))
  (! (let ((a!1 (exists ((%1 T1)) (! (= (not (Rmem l1 %1)) (= %1 %0)) :qid itp)))
           (a!2 (forall ((bv0 T1))
                  (! (= (Rmem v bv0) (or (Rmem l2 bv0) (= bv0 %0)))
                     :pattern ((Rmem v bv0))
                     :pattern ((Rmem l2 bv0))))))
       (or a!1 a!2))
     :qid itp))

Can you say what version/architecture you're using?