;; 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 i100::Index)
(define i101::Index)
(define i102::Index)
(define i103::Index)
(define i104::Index)
(define i105::Index)
(define i106::Index)
(define i107::Index)
(define i108::Index)
(define i109::Index)
(define i110::Index)
(define i111::Index)
(define i112::Index)
(define i113::Index)
(define i114::Index)
(define i115::Index)
(define i116::Index)
(define i117::Index)
(define i118::Index)
(define i119::Index)
(define i120::Index)
(define i121::Index)
(define i122::Index)
(define i123::Index)
(define i124::Index)
(define i125::Index)
(define i126::Index)
(define i127::Index)
(define i128::Index)
(define i129::Index)
(define i130::Index)
(define i131::Index)
(define i132::Index)
(define i133::Index)
(define i134::Index)
(define i135::Index)
(define i136::Index)
(define i137::Index)
(define i138::Index)
(define i139::Index)
(define i140::Index)
(define i141::Index)
(define i142::Index)
(define i143::Index)
(define i144::Index)
(define i145::Index)
(define i146::Index)
(define i147::Index)
(define i148::Index)
(define i149::Index)
(define i150::Index)
(define i151::Index)
(define i152::Index)
(define i153::Index)
(define i154::Index)
(define i155::Index)
(define i156::Index)
(define i157::Index)
(define i158::Index)
(define i159::Index)
(define i160::Index)
(define i161::Index)
(define i162::Index)
(define i163::Index)
(define i164::Index)
(define i165::Index)
(define i166::Index)
(define i167::Index)
(define i168::Index)
(define i169::Index)
(define i170::Index)
(define i171::Index)
(define i172::Index)
(define i173::Index)
(define i174::Index)
(define i175::Index)
(define i176::Index)
(define i177::Index)
(define i178::Index)
(define i179::Index)
(define i180::Index)
(define i181::Index)
(define i182::Index)
(define i183::Index)
(define i184::Index)
(define i185::Index)
(define i186::Index)
(define i187::Index)
(define i188::Index)
(define i189::Index)
(define i190::Index)
(define i191::Index)
(define i192::Index)
(define i193::Index)
(define i194::Index)
(define i195::Index)
(define i196::Index)
(define i197::Index)
(define i198::Index)
(define i199::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)
(define x100::Element)
(define x101::Element)
(define x102::Element)
(define x103::Element)
(define x104::Element)
(define x105::Element)
(define x106::Element)
(define x107::Element)
(define x108::Element)
(define x109::Element)
(define x110::Element)
(define x111::Element)
(define x112::Element)
(define x113::Element)
(define x114::Element)
(define x115::Element)
(define x116::Element)
(define x117::Element)
(define x118::Element)
(define x119::Element)
(define x120::Element)
(define x121::Element)
(define x122::Element)
(define x123::Element)
(define x124::Element)
(define x125::Element)
(define x126::Element)
(define x127::Element)
(define x128::Element)
(define x129::Element)
(define x130::Element)
(define x131::Element)
(define x132::Element)
(define x133::Element)
(define x134::Element)
(define x135::Element)
(define x136::Element)
(define x137::Element)
(define x138::Element)
(define x139::Element)
(define x140::Element)
(define x141::Element)
(define x142::Element)
(define x143::Element)
(define x144::Element)
(define x145::Element)
(define x146::Element)
(define x147::Element)
(define x148::Element)
(define x149::Element)
(define x150::Element)
(define x151::Element)
(define x152::Element)
(define x153::Element)
(define x154::Element)
(define x155::Element)
(define x156::Element)
(define x157::Element)
(define x158::Element)
(define x159::Element)
(define x160::Element)
(define x161::Element)
(define x162::Element)
(define x163::Element)
(define x164::Element)
(define x165::Element)
(define x166::Element)
(define x167::Element)
(define x168::Element)
(define x169::Element)
(define x170::Element)
(define x171::Element)
(define x172::Element)
(define x173::Element)
(define x174::Element)
(define x175::Element)
(define x176::Element)
(define x177::Element)
(define x178::Element)
(define x179::Element)
(define x180::Element)
(define x181::Element)
(define x182::Element)
(define x183::Element)
(define x184::Element)
(define x185::Element)
(define x186::Element)
(define x187::Element)
(define x188::Element)
(define x189::Element)
(define x190::Element)
(define x191::Element)
(define x192::Element)
(define x193::Element)
(define x194::Element)
(define x195::Element)
(define x196::Element)
(define x197::Element)
(define x198::Element)
(define x199::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 (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) (i100) x100) (i101) x101) (i102) x102) (i103) x103) (i104) x104) (i105) x105) (i106) x106) (i107) x107) (i108) x108) (i109) x109) (i110) x110) (i111) x111) (i112) x112) (i113) x113) (i114) x114) (i115) x115) (i116) x116) (i117) x117) (i118) x118) (i119) x119) (i120) x120) (i121) x121) (i122) x122) (i123) x123) (i124) x124) (i125) x125) (i126) x126) (i127) x127) (i128) x128) (i129) x129) (i130) x130) (i131) x131) (i132) x132) (i133) x133) (i134) x134) (i135) x135) (i136) x136) (i137) x137) (i138) x138) (i139) x139) (i140) x140) (i141) x141) (i142) x142) (i143) x143) (i144) x144) (i145) x145) (i146) x146) (i147) x147) (i148) x148) (i149) x149) (i150) x150) (i151) x151) (i152) x152) (i153) x153) (i154) x154) (i155) x155) (i156) x156) (i157) x157) (i158) x158) (i159) x159) (i160) x160) (i161) x161) (i162) x162) (i163) x163) (i164) x164) (i165) x165) (i166) x166) (i167) x167) (i168) x168) (i169) x169) (i170) x170) (i171) x171) (i172) x172) (i173) x173) (i174) x174) (i175) x175) (i176) x176) (i177) x177) (i178) x178) (i179) x179) (i180) x180) (i181) x181) (i182) x182) (i183) x183) (i184) x184) (i185) x185) (i186) x186) (i187) x187) (i188) x188) (i189) x189) (i190) x190) (i191) x191) (i192) x192) (i193) x193) (i194) x194) (i195) x195) (i196) x196) (i197) x197) (i198) x198) (i199) x199)
(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 (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) (i100) x100) (i101) x101) (i102) x102) (i103) x103) (i104) x104) (i105) x105) (i106) x106) (i107) x107) (i108) x108) (i109) x109) (i110) x110) (i111) x111) (i112) x112) (i113) x113) (i114) x114) (i115) x115) (i116) x116) (i117) x117) (i118) x118) (i119) x119) (i120) x120) (i121) x121) (i122) x122) (i123) x123) (i124) x124) (i125) x125) (i126) x126) (i127) x127) (i128) x128) (i129) x129) (i130) x130) (i131) x131) (i132) x132) (i133) x133) (i134) x134) (i135) x135) (i136) x136) (i137) x137) (i138) x138) (i139) x139) (i140) x140) (i141) x141) (i142) x142) (i143) x143) (i144) x144) (i145) x145) (i146) x146) (i147) x147) (i148) x148) (i149) x149) (i150) x150) (i151) x151) (i152) x152) (i153) x153) (i154) x154) (i155) x155) (i156) x156) (i157) x157) (i158) x158) (i159) x159) (i160) x160) (i161) x161) (i162) x162) (i163) x163) (i164) x164) (i165) x165) (i166) x166) (i167) x167) (i168) x168) (i169) x169) (i170) x170) (i171) x171) (i172) x172) (i173) x173) (i174) x174) (i175) x175) (i176) x176) (i177) x177) (i178) x178) (i179) x179) (i180) x180) (i181) x181) (i182) x182) (i183) x183) (i184) x184) (i185) x185) (i186) x186) (i187) x187) (i188) x188) (i189) x189) (i190) x190) (i191) x191) (i192) x192) (i193) x193) (i194) x194) (i195) x195) (i196) x196) (i197) x197) (i198) x198) (i199) x199)
)))

(check)
(show-model)