RiSE4fun samples for iZ3List of built-in samples for the iZ3 in RiSE4funen-US<a target='_blank' href='https://go.microsoft.com/?linkid=2028325'>Contact Us</a>| <a target='_blank' href='https://go.microsoft.com/fwlink/?LinkId=521839'>Privacy &amp; Cookies</a> | <a target='_blank' href='https://go.microsoft.com/fwlink/?LinkID=246338'>Terms of Use</a> | <a target='_blank' href='https://go.microsoft.com/fwlink/?LinkId=506942 '>Trademarks</a>| &copy; 2017 Microsofthttps://rise4fun.com//Images/Rise.gifRiSE4fun samples for iZ3https://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))) https://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)))) https://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)) https://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)))) https://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))))) https://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))))) https://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))) https://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)))))