RiSE4fun samples for iZ3List of built-in samples for the iZ3 in RiSE4funen-USrise4fun © 2017 Microsoft Corporationhttp://rise4fun.com//Images/Rise.gifRiSE4fun samples for iZ3http://rise4fun.com/iZ3/even_oddeven_odd(declare-const x Int) (declare-const y Int) (declare-const z Int) (compute-interpolant (= y (* 2 x)) (= y (+ (* 2 z) 1))) http://rise4fun.com/iZ3/simplesimple(declare-const a Int) (declare-const b Int) (declare-const c Int) (declare-const d Int) (compute-interpolant (and (= a b) (= a c)) (and (= b d) (not (= c d)))) http://rise4fun.com/iZ3/quantifierquantifier(declare-const i Int) (declare-fun P (Int) Bool) (declare-fun Q (Int) Bool) (compute-interpolant (and (forall ((x Int)) (=> (Q x) (P x))) (forall ((x Int)) (not (P x)))) (Q i)) http://rise4fun.com/iZ3/sequencesequence(declare-const a Int) (declare-const b Int) (declare-const c Int) (declare-const d Int) (declare-const e Int) (compute-interpolant (and (= a b) (= a c)) (= c d) (and (= b e) (not (= d e)))) http://rise4fun.com/iZ3/incrementalincremental(declare-const a Int) (declare-const b Int) (declare-const c Int) (declare-const d Int) (compute-interpolant (and (= b c) (interp (and (= a 0) (= a b))) (interp (and (= c d) (= d 1))))) http://rise4fun.com/iZ3/treetree(declare-const a Int) (declare-const b Int) (declare-const c Int) (declare-const d Int) (compute-interpolant (and (= b c) (interp (and (= a 0) (= a b))) (interp (and (= c d) (= d 1))))) http://rise4fun.com/iZ3/two_storetwo_store(declare-const x Int) (declare-const y Int) (declare-const z Int) (declare-const a (Array Int Int)) (declare-const b (Array Int Int)) (compute-interpolant (= b (store (store a x 0) y 0)) (and (= z x) (= (select b z) 1))) http://rise4fun.com/iZ3/equalityequality(declare-const a Int) (declare-const b Int) (declare-const c Int) (declare-const d Int) (declare-fun f (Int) Int) (declare-fun g (Int) Int) (compute-interpolant (and (= (f a) c) (= (f b) d)) (and (= a b) (not (= (g c) (g d)))))