;; test for Yices (taken from SMT 2008 paper by Sava Krstic et al.)

(define-type Index)
(define-type Element)
(define-type Array (-> Index Element))

(define a::Array)
(define b::Array)
(define i0::Index)
(define i1::Index)
(define i2::Index)
(define i3::Index)
(define i4::Index)
(define i5::Index)
(define i6::Index)
(define i7::Index)
(define i8::Index)
(define i9::Index)
(define i10::Index)
(define i11::Index)
(define i12::Index)
(define i13::Index)
(define i14::Index)
(define i15::Index)
(define i16::Index)
(define i17::Index)
(define i18::Index)
(define i19::Index)
(define i20::Index)
(define i21::Index)
(define i22::Index)
(define i23::Index)
(define i24::Index)
(define i25::Index)
(define i26::Index)
(define i27::Index)
(define i28::Index)
(define i29::Index)
(define i30::Index)
(define i31::Index)
(define i32::Index)
(define i33::Index)
(define i34::Index)
(define i35::Index)
(define i36::Index)
(define i37::Index)
(define i38::Index)
(define i39::Index)
(define i40::Index)
(define i41::Index)
(define i42::Index)
(define i43::Index)
(define i44::Index)
(define i45::Index)
(define i46::Index)
(define i47::Index)
(define i48::Index)
(define i49::Index)
(define i50::Index)
(define i51::Index)
(define i52::Index)
(define i53::Index)
(define i54::Index)
(define i55::Index)
(define i56::Index)
(define i57::Index)
(define i58::Index)
(define i59::Index)
(define i60::Index)
(define i61::Index)
(define i62::Index)
(define i63::Index)
(define i64::Index)
(define i65::Index)
(define i66::Index)
(define i67::Index)
(define i68::Index)
(define i69::Index)
(define i70::Index)
(define i71::Index)
(define i72::Index)
(define i73::Index)
(define i74::Index)
(define i75::Index)
(define i76::Index)
(define i77::Index)
(define i78::Index)
(define i79::Index)
(define i80::Index)
(define i81::Index)
(define i82::Index)
(define i83::Index)
(define i84::Index)
(define i85::Index)
(define i86::Index)
(define i87::Index)
(define i88::Index)
(define i89::Index)
(define i90::Index)
(define i91::Index)
(define i92::Index)
(define i93::Index)
(define i94::Index)
(define i95::Index)
(define i96::Index)
(define i97::Index)
(define i98::Index)
(define i99::Index)
(define x0::Element)
(define x1::Element)
(define x2::Element)
(define x3::Element)
(define x4::Element)
(define x5::Element)
(define x6::Element)
(define x7::Element)
(define x8::Element)
(define x9::Element)
(define x10::Element)
(define x11::Element)
(define x12::Element)
(define x13::Element)
(define x14::Element)
(define x15::Element)
(define x16::Element)
(define x17::Element)
(define x18::Element)
(define x19::Element)
(define x20::Element)
(define x21::Element)
(define x22::Element)
(define x23::Element)
(define x24::Element)
(define x25::Element)
(define x26::Element)
(define x27::Element)
(define x28::Element)
(define x29::Element)
(define x30::Element)
(define x31::Element)
(define x32::Element)
(define x33::Element)
(define x34::Element)
(define x35::Element)
(define x36::Element)
(define x37::Element)
(define x38::Element)
(define x39::Element)
(define x40::Element)
(define x41::Element)
(define x42::Element)
(define x43::Element)
(define x44::Element)
(define x45::Element)
(define x46::Element)
(define x47::Element)
(define x48::Element)
(define x49::Element)
(define x50::Element)
(define x51::Element)
(define x52::Element)
(define x53::Element)
(define x54::Element)
(define x55::Element)
(define x56::Element)
(define x57::Element)
(define x58::Element)
(define x59::Element)
(define x60::Element)
(define x61::Element)
(define x62::Element)
(define x63::Element)
(define x64::Element)
(define x65::Element)
(define x66::Element)
(define x67::Element)
(define x68::Element)
(define x69::Element)
(define x70::Element)
(define x71::Element)
(define x72::Element)
(define x73::Element)
(define x74::Element)
(define x75::Element)
(define x76::Element)
(define x77::Element)
(define x78::Element)
(define x79::Element)
(define x80::Element)
(define x81::Element)
(define x82::Element)
(define x83::Element)
(define x84::Element)
(define x85::Element)
(define x86::Element)
(define x87::Element)
(define x88::Element)
(define x89::Element)
(define x90::Element)
(define x91::Element)
(define x92::Element)
(define x93::Element)
(define x94::Element)
(define x95::Element)
(define x96::Element)
(define x97::Element)
(define x98::Element)
(define x99::Element)


(assert (not (= 
(update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update a (i0) x0) (i1) x1) (i2) x2) (i3) x3) (i4) x4) (i5) x5) (i6) x6) (i7) x7) (i8) x8) (i9) x9) (i10) x10) (i11) x11) (i12) x12) (i13) x13) (i14) x14) (i15) x15) (i16) x16) (i17) x17) (i18) x18) (i19) x19) (i20) x20) (i21) x21) (i22) x22) (i23) x23) (i24) x24) (i25) x25) (i26) x26) (i27) x27) (i28) x28) (i29) x29) (i30) x30) (i31) x31) (i32) x32) (i33) x33) (i34) x34) (i35) x35) (i36) x36) (i37) x37) (i38) x38) (i39) x39) (i40) x40) (i41) x41) (i42) x42) (i43) x43) (i44) x44) (i45) x45) (i46) x46) (i47) x47) (i48) x48) (i49) x49) (i50) x50) (i51) x51) (i52) x52) (i53) x53) (i54) x54) (i55) x55) (i56) x56) (i57) x57) (i58) x58) (i59) x59) (i60) x60) (i61) x61) (i62) x62) (i63) x63) (i64) x64) (i65) x65) (i66) x66) (i67) x67) (i68) x68) (i69) x69) (i70) x70) (i71) x71) (i72) x72) (i73) x73) (i74) x74) (i75) x75) (i76) x76) (i77) x77) (i78) x78) (i79) x79) (i80) x80) (i81) x81) (i82) x82) (i83) x83) (i84) x84) (i85) x85) (i86) x86) (i87) x87) (i88) x88) (i89) x89) (i90) x90) (i91) x91) (i92) x92) (i93) x93) (i94) x94) (i95) x95) (i96) x96) (i97) x97) (i98) x98) (i99) x99)
(update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update (update b (i0) x0) (i1) x1) (i2) x2) (i3) x3) (i4) x4) (i5) x5) (i6) x6) (i7) x7) (i8) x8) (i9) x9) (i10) x10) (i11) x11) (i12) x12) (i13) x13) (i14) x14) (i15) x15) (i16) x16) (i17) x17) (i18) x18) (i19) x19) (i20) x20) (i21) x21) (i22) x22) (i23) x23) (i24) x24) (i25) x25) (i26) x26) (i27) x27) (i28) x28) (i29) x29) (i30) x30) (i31) x31) (i32) x32) (i33) x33) (i34) x34) (i35) x35) (i36) x36) (i37) x37) (i38) x38) (i39) x39) (i40) x40) (i41) x41) (i42) x42) (i43) x43) (i44) x44) (i45) x45) (i46) x46) (i47) x47) (i48) x48) (i49) x49) (i50) x50) (i51) x51) (i52) x52) (i53) x53) (i54) x54) (i55) x55) (i56) x56) (i57) x57) (i58) x58) (i59) x59) (i60) x60) (i61) x61) (i62) x62) (i63) x63) (i64) x64) (i65) x65) (i66) x66) (i67) x67) (i68) x68) (i69) x69) (i70) x70) (i71) x71) (i72) x72) (i73) x73) (i74) x74) (i75) x75) (i76) x76) (i77) x77) (i78) x78) (i79) x79) (i80) x80) (i81) x81) (i82) x82) (i83) x83) (i84) x84) (i85) x85) (i86) x86) (i87) x87) (i88) x88) (i89) x89) (i90) x90) (i91) x91) (i92) x92) (i93) x93) (i94) x94) (i95) x95) (i96) x96) (i97) x97) (i98) x98) (i99) x99))))

(check)
(show-model)