diff --git a/jbmc/regression/jbmc/lots_of_local_variables/TooManyLocals.class b/jbmc/regression/jbmc/lots_of_local_variables/TooManyLocals.class
index b72240605da..da3698b1382 100644
Binary files a/jbmc/regression/jbmc/lots_of_local_variables/TooManyLocals.class and b/jbmc/regression/jbmc/lots_of_local_variables/TooManyLocals.class differ
diff --git a/jbmc/regression/jbmc/lots_of_local_variables/TooManyLocals.java b/jbmc/regression/jbmc/lots_of_local_variables/TooManyLocals.java
index 512a1d0a6d4..4ff9c0ddca8 100644
--- a/jbmc/regression/jbmc/lots_of_local_variables/TooManyLocals.java
+++ b/jbmc/regression/jbmc/lots_of_local_variables/TooManyLocals.java
@@ -1,6 +1,6 @@
 public class TooManyLocals {
   public static void test() {
-    int [] allInts = new int[256];
+    int allInts = 0;
     int i0 = 0;
     int i1 = 1;
     int i2 = 2;
@@ -257,262 +257,264 @@ public static void test() {
     int i253 = 253;
     int i254 = 254;
     int i255 = 255;
-    allInts[0] = i0;
-    allInts[1] = i1;
-    allInts[2] = i2;
-    allInts[3] = i3;
-    allInts[4] = i4;
-    allInts[5] = i5;
-    allInts[6] = i6;
-    allInts[7] = i7;
-    allInts[8] = i8;
-    allInts[9] = i9;
-    allInts[10] = i10;
-    allInts[11] = i11;
-    allInts[12] = i12;
-    allInts[13] = i13;
-    allInts[14] = i14;
-    allInts[15] = i15;
-    allInts[16] = i16;
-    allInts[17] = i17;
-    allInts[18] = i18;
-    allInts[19] = i19;
-    allInts[20] = i20;
-    allInts[21] = i21;
-    allInts[22] = i22;
-    allInts[23] = i23;
-    allInts[24] = i24;
-    allInts[25] = i25;
-    allInts[26] = i26;
-    allInts[27] = i27;
-    allInts[28] = i28;
-    allInts[29] = i29;
-    allInts[30] = i30;
-    allInts[31] = i31;
-    allInts[32] = i32;
-    allInts[33] = i33;
-    allInts[34] = i34;
-    allInts[35] = i35;
-    allInts[36] = i36;
-    allInts[37] = i37;
-    allInts[38] = i38;
-    allInts[39] = i39;
-    allInts[40] = i40;
-    allInts[41] = i41;
-    allInts[42] = i42;
-    allInts[43] = i43;
-    allInts[44] = i44;
-    allInts[45] = i45;
-    allInts[46] = i46;
-    allInts[47] = i47;
-    allInts[48] = i48;
-    allInts[49] = i49;
-    allInts[50] = i50;
-    allInts[51] = i51;
-    allInts[52] = i52;
-    allInts[53] = i53;
-    allInts[54] = i54;
-    allInts[55] = i55;
-    allInts[56] = i56;
-    allInts[57] = i57;
-    allInts[58] = i58;
-    allInts[59] = i59;
-    allInts[60] = i60;
-    allInts[61] = i61;
-    allInts[62] = i62;
-    allInts[63] = i63;
-    allInts[64] = i64;
-    allInts[65] = i65;
-    allInts[66] = i66;
-    allInts[67] = i67;
-    allInts[68] = i68;
-    allInts[69] = i69;
-    allInts[70] = i70;
-    allInts[71] = i71;
-    allInts[72] = i72;
-    allInts[73] = i73;
-    allInts[74] = i74;
-    allInts[75] = i75;
-    allInts[76] = i76;
-    allInts[77] = i77;
-    allInts[78] = i78;
-    allInts[79] = i79;
-    allInts[80] = i80;
-    allInts[81] = i81;
-    allInts[82] = i82;
-    allInts[83] = i83;
-    allInts[84] = i84;
-    allInts[85] = i85;
-    allInts[86] = i86;
-    allInts[87] = i87;
-    allInts[88] = i88;
-    allInts[89] = i89;
-    allInts[90] = i90;
-    allInts[91] = i91;
-    allInts[92] = i92;
-    allInts[93] = i93;
-    allInts[94] = i94;
-    allInts[95] = i95;
-    allInts[96] = i96;
-    allInts[97] = i97;
-    allInts[98] = i98;
-    allInts[99] = i99;
-    allInts[100] = i100;
-    allInts[101] = i101;
-    allInts[102] = i102;
-    allInts[103] = i103;
-    allInts[104] = i104;
-    allInts[105] = i105;
-    allInts[106] = i106;
-    allInts[107] = i107;
-    allInts[108] = i108;
-    allInts[109] = i109;
-    allInts[110] = i110;
-    allInts[111] = i111;
-    allInts[112] = i112;
-    allInts[113] = i113;
-    allInts[114] = i114;
-    allInts[115] = i115;
-    allInts[116] = i116;
-    allInts[117] = i117;
-    allInts[118] = i118;
-    allInts[119] = i119;
-    allInts[120] = i120;
-    allInts[121] = i121;
-    allInts[122] = i122;
-    allInts[123] = i123;
-    allInts[124] = i124;
-    allInts[125] = i125;
-    allInts[126] = i126;
-    allInts[127] = i127;
-    allInts[128] = i128;
-    allInts[129] = i129;
-    allInts[130] = i130;
-    allInts[131] = i131;
-    allInts[132] = i132;
-    allInts[133] = i133;
-    allInts[134] = i134;
-    allInts[135] = i135;
-    allInts[136] = i136;
-    allInts[137] = i137;
-    allInts[138] = i138;
-    allInts[139] = i139;
-    allInts[140] = i140;
-    allInts[141] = i141;
-    allInts[142] = i142;
-    allInts[143] = i143;
-    allInts[144] = i144;
-    allInts[145] = i145;
-    allInts[146] = i146;
-    allInts[147] = i147;
-    allInts[148] = i148;
-    allInts[149] = i149;
-    allInts[150] = i150;
-    allInts[151] = i151;
-    allInts[152] = i152;
-    allInts[153] = i153;
-    allInts[154] = i154;
-    allInts[155] = i155;
-    allInts[156] = i156;
-    allInts[157] = i157;
-    allInts[158] = i158;
-    allInts[159] = i159;
-    allInts[160] = i160;
-    allInts[161] = i161;
-    allInts[162] = i162;
-    allInts[163] = i163;
-    allInts[164] = i164;
-    allInts[165] = i165;
-    allInts[166] = i166;
-    allInts[167] = i167;
-    allInts[168] = i168;
-    allInts[169] = i169;
-    allInts[170] = i170;
-    allInts[171] = i171;
-    allInts[172] = i172;
-    allInts[173] = i173;
-    allInts[174] = i174;
-    allInts[175] = i175;
-    allInts[176] = i176;
-    allInts[177] = i177;
-    allInts[178] = i178;
-    allInts[179] = i179;
-    allInts[180] = i180;
-    allInts[181] = i181;
-    allInts[182] = i182;
-    allInts[183] = i183;
-    allInts[184] = i184;
-    allInts[185] = i185;
-    allInts[186] = i186;
-    allInts[187] = i187;
-    allInts[188] = i188;
-    allInts[189] = i189;
-    allInts[190] = i190;
-    allInts[191] = i191;
-    allInts[192] = i192;
-    allInts[193] = i193;
-    allInts[194] = i194;
-    allInts[195] = i195;
-    allInts[196] = i196;
-    allInts[197] = i197;
-    allInts[198] = i198;
-    allInts[199] = i199;
-    allInts[200] = i200;
-    allInts[201] = i201;
-    allInts[202] = i202;
-    allInts[203] = i203;
-    allInts[204] = i204;
-    allInts[205] = i205;
-    allInts[206] = i206;
-    allInts[207] = i207;
-    allInts[208] = i208;
-    allInts[209] = i209;
-    allInts[210] = i210;
-    allInts[211] = i211;
-    allInts[212] = i212;
-    allInts[213] = i213;
-    allInts[214] = i214;
-    allInts[215] = i215;
-    allInts[216] = i216;
-    allInts[217] = i217;
-    allInts[218] = i218;
-    allInts[219] = i219;
-    allInts[220] = i220;
-    allInts[221] = i221;
-    allInts[222] = i222;
-    allInts[223] = i223;
-    allInts[224] = i224;
-    allInts[225] = i225;
-    allInts[226] = i226;
-    allInts[227] = i227;
-    allInts[228] = i228;
-    allInts[229] = i229;
-    allInts[230] = i230;
-    allInts[231] = i231;
-    allInts[232] = i232;
-    allInts[233] = i233;
-    allInts[234] = i234;
-    allInts[235] = i235;
-    allInts[236] = i236;
-    allInts[237] = i237;
-    allInts[238] = i238;
-    allInts[239] = i239;
-    allInts[240] = i240;
-    allInts[241] = i241;
-    allInts[242] = i242;
-    allInts[243] = i243;
-    allInts[244] = i244;
-    allInts[245] = i245;
-    allInts[246] = i246;
-    allInts[247] = i247;
-    allInts[248] = i248;
-    allInts[249] = i249;
-    allInts[250] = i250;
-    allInts[251] = i251;
-    allInts[252] = i252;
-    allInts[253] = i253;
-    allInts[254] = i254;
-    allInts[255] = i255;
-    assert(allInts[255] + allInts[0] == 255);
+    int i256 = 256;
+    allInts += i0;
+    allInts += i1;
+    allInts += i2;
+    allInts += i3;
+    allInts += i4;
+    allInts += i5;
+    allInts += i6;
+    allInts += i7;
+    allInts += i8;
+    allInts += i9;
+    allInts += i10;
+    allInts += i11;
+    allInts += i12;
+    allInts += i13;
+    allInts += i14;
+    allInts += i15;
+    allInts += i16;
+    allInts += i17;
+    allInts += i18;
+    allInts += i19;
+    allInts += i20;
+    allInts += i21;
+    allInts += i22;
+    allInts += i23;
+    allInts += i24;
+    allInts += i25;
+    allInts += i26;
+    allInts += i27;
+    allInts += i28;
+    allInts += i29;
+    allInts += i30;
+    allInts += i31;
+    allInts += i32;
+    allInts += i33;
+    allInts += i34;
+    allInts += i35;
+    allInts += i36;
+    allInts += i37;
+    allInts += i38;
+    allInts += i39;
+    allInts += i40;
+    allInts += i41;
+    allInts += i42;
+    allInts += i43;
+    allInts += i44;
+    allInts += i45;
+    allInts += i46;
+    allInts += i47;
+    allInts += i48;
+    allInts += i49;
+    allInts += i50;
+    allInts += i51;
+    allInts += i52;
+    allInts += i53;
+    allInts += i54;
+    allInts += i55;
+    allInts += i56;
+    allInts += i57;
+    allInts += i58;
+    allInts += i59;
+    allInts += i60;
+    allInts += i61;
+    allInts += i62;
+    allInts += i63;
+    allInts += i64;
+    allInts += i65;
+    allInts += i66;
+    allInts += i67;
+    allInts += i68;
+    allInts += i69;
+    allInts += i70;
+    allInts += i71;
+    allInts += i72;
+    allInts += i73;
+    allInts += i74;
+    allInts += i75;
+    allInts += i76;
+    allInts += i77;
+    allInts += i78;
+    allInts += i79;
+    allInts += i80;
+    allInts += i81;
+    allInts += i82;
+    allInts += i83;
+    allInts += i84;
+    allInts += i85;
+    allInts += i86;
+    allInts += i87;
+    allInts += i88;
+    allInts += i89;
+    allInts += i90;
+    allInts += i91;
+    allInts += i92;
+    allInts += i93;
+    allInts += i94;
+    allInts += i95;
+    allInts += i96;
+    allInts += i97;
+    allInts += i98;
+    allInts += i99;
+    allInts += i100;
+    allInts += i101;
+    allInts += i102;
+    allInts += i103;
+    allInts += i104;
+    allInts += i105;
+    allInts += i106;
+    allInts += i107;
+    allInts += i108;
+    allInts += i109;
+    allInts += i110;
+    allInts += i111;
+    allInts += i112;
+    allInts += i113;
+    allInts += i114;
+    allInts += i115;
+    allInts += i116;
+    allInts += i117;
+    allInts += i118;
+    allInts += i119;
+    allInts += i120;
+    allInts += i121;
+    allInts += i122;
+    allInts += i123;
+    allInts += i124;
+    allInts += i125;
+    allInts += i126;
+    allInts += i127;
+    allInts += i128;
+    allInts += i129;
+    allInts += i130;
+    allInts += i131;
+    allInts += i132;
+    allInts += i133;
+    allInts += i134;
+    allInts += i135;
+    allInts += i136;
+    allInts += i137;
+    allInts += i138;
+    allInts += i139;
+    allInts += i140;
+    allInts += i141;
+    allInts += i142;
+    allInts += i143;
+    allInts += i144;
+    allInts += i145;
+    allInts += i146;
+    allInts += i147;
+    allInts += i148;
+    allInts += i149;
+    allInts += i150;
+    allInts += i151;
+    allInts += i152;
+    allInts += i153;
+    allInts += i154;
+    allInts += i155;
+    allInts += i156;
+    allInts += i157;
+    allInts += i158;
+    allInts += i159;
+    allInts += i160;
+    allInts += i161;
+    allInts += i162;
+    allInts += i163;
+    allInts += i164;
+    allInts += i165;
+    allInts += i166;
+    allInts += i167;
+    allInts += i168;
+    allInts += i169;
+    allInts += i170;
+    allInts += i171;
+    allInts += i172;
+    allInts += i173;
+    allInts += i174;
+    allInts += i175;
+    allInts += i176;
+    allInts += i177;
+    allInts += i178;
+    allInts += i179;
+    allInts += i180;
+    allInts += i181;
+    allInts += i182;
+    allInts += i183;
+    allInts += i184;
+    allInts += i185;
+    allInts += i186;
+    allInts += i187;
+    allInts += i188;
+    allInts += i189;
+    allInts += i190;
+    allInts += i191;
+    allInts += i192;
+    allInts += i193;
+    allInts += i194;
+    allInts += i195;
+    allInts += i196;
+    allInts += i197;
+    allInts += i198;
+    allInts += i199;
+    allInts += i200;
+    allInts += i201;
+    allInts += i202;
+    allInts += i203;
+    allInts += i204;
+    allInts += i205;
+    allInts += i206;
+    allInts += i207;
+    allInts += i208;
+    allInts += i209;
+    allInts += i210;
+    allInts += i211;
+    allInts += i212;
+    allInts += i213;
+    allInts += i214;
+    allInts += i215;
+    allInts += i216;
+    allInts += i217;
+    allInts += i218;
+    allInts += i219;
+    allInts += i220;
+    allInts += i221;
+    allInts += i222;
+    allInts += i223;
+    allInts += i224;
+    allInts += i225;
+    allInts += i226;
+    allInts += i227;
+    allInts += i228;
+    allInts += i229;
+    allInts += i230;
+    allInts += i231;
+    allInts += i232;
+    allInts += i233;
+    allInts += i234;
+    allInts += i235;
+    allInts += i236;
+    allInts += i237;
+    allInts += i238;
+    allInts += i239;
+    allInts += i240;
+    allInts += i241;
+    allInts += i242;
+    allInts += i243;
+    allInts += i244;
+    allInts += i245;
+    allInts += i246;
+    allInts += i247;
+    allInts += i248;
+    allInts += i249;
+    allInts += i250;
+    allInts += i251;
+    allInts += i252;
+    allInts += i253;
+    allInts += i254;
+    allInts += i255;
+    allInts += i256;
+    assert(allInts == 257 * 128);
   }
 }
diff --git a/jbmc/regression/jbmc/lots_of_local_variables/test.desc b/jbmc/regression/jbmc/lots_of_local_variables/test.desc
index cbe9e269ccc..3f48d3e2a68 100644
--- a/jbmc/regression/jbmc/lots_of_local_variables/test.desc
+++ b/jbmc/regression/jbmc/lots_of_local_variables/test.desc
@@ -2,6 +2,5 @@ CORE
 TooManyLocals.class
 --function TooManyLocals.test
 VERIFICATION SUCCESSFUL
-\[java::TooManyLocals\.test:\(\)V\.assertion\.1\] .*: SUCCESS
 ^EXIT=0$
 ^SIGNAL=0$