diff --git a/regression/cbmc-java/lots_local_variables_manual/ManyLocalVariables.class b/regression/cbmc-java/lots_local_variables_manual/ManyLocalVariables.class
new file mode 100644
index 00000000000..e33d34c568a
Binary files /dev/null and b/regression/cbmc-java/lots_local_variables_manual/ManyLocalVariables.class differ
diff --git a/regression/cbmc-java/lots_local_variables_manual/ManyLocalVariables.j b/regression/cbmc-java/lots_local_variables_manual/ManyLocalVariables.j
new file mode 100644
index 00000000000..78ae053aeb8
--- /dev/null
+++ b/regression/cbmc-java/lots_local_variables_manual/ManyLocalVariables.j
@@ -0,0 +1,36 @@
+; This generates a class file that attempts to access local variables indexed
+; at 255, 256 and 65534
+; The class file is generated from this file using the following command:
+; java -jar jasmin.jar ManyLocalVariables.j
+; The jasmin jar file can be obtained from: http://jasmin.sourceforge.net/
+
+.class public ManyLocalVariables
+.super java/lang/Object
+
+.method public static test()I
+  .limit stack 10
+  .limit locals 65535
+  .line 1
+   iconst_1
+   istore 1
+
+   iconst_1
+   istore 255
+
+   iconst_1
+   istore_w 256
+
+   iconst_1
+   istore_w 65534
+
+   iload 1
+   iload 255
+   iload_w 256
+   iload_w 65534
+
+   iadd
+   iadd
+   iadd
+
+   ireturn
+.end method
diff --git a/regression/cbmc-java/lots_local_variables_manual/test.desc b/regression/cbmc-java/lots_local_variables_manual/test.desc
new file mode 100644
index 00000000000..4d5140cf86d
--- /dev/null
+++ b/regression/cbmc-java/lots_local_variables_manual/test.desc
@@ -0,0 +1,4 @@
+CORE
+ManyLocalVariables.class
+--function ManyLocalVariables.test
+VERIFICATION SUCCESSFUL
diff --git a/regression/cbmc-java/lots_of_local_variables/TooManyLocals.class b/regression/cbmc-java/lots_of_local_variables/TooManyLocals.class
new file mode 100644
index 00000000000..b72240605da
Binary files /dev/null and b/regression/cbmc-java/lots_of_local_variables/TooManyLocals.class differ
diff --git a/regression/cbmc-java/lots_of_local_variables/TooManyLocals.java b/regression/cbmc-java/lots_of_local_variables/TooManyLocals.java
new file mode 100644
index 00000000000..512a1d0a6d4
--- /dev/null
+++ b/regression/cbmc-java/lots_of_local_variables/TooManyLocals.java
@@ -0,0 +1,518 @@
+public class TooManyLocals {
+  public static void test() {
+    int [] allInts = new int[256];
+    int i0 = 0;
+    int i1 = 1;
+    int i2 = 2;
+    int i3 = 3;
+    int i4 = 4;
+    int i5 = 5;
+    int i6 = 6;
+    int i7 = 7;
+    int i8 = 8;
+    int i9 = 9;
+    int i10 = 10;
+    int i11 = 11;
+    int i12 = 12;
+    int i13 = 13;
+    int i14 = 14;
+    int i15 = 15;
+    int i16 = 16;
+    int i17 = 17;
+    int i18 = 18;
+    int i19 = 19;
+    int i20 = 20;
+    int i21 = 21;
+    int i22 = 22;
+    int i23 = 23;
+    int i24 = 24;
+    int i25 = 25;
+    int i26 = 26;
+    int i27 = 27;
+    int i28 = 28;
+    int i29 = 29;
+    int i30 = 30;
+    int i31 = 31;
+    int i32 = 32;
+    int i33 = 33;
+    int i34 = 34;
+    int i35 = 35;
+    int i36 = 36;
+    int i37 = 37;
+    int i38 = 38;
+    int i39 = 39;
+    int i40 = 40;
+    int i41 = 41;
+    int i42 = 42;
+    int i43 = 43;
+    int i44 = 44;
+    int i45 = 45;
+    int i46 = 46;
+    int i47 = 47;
+    int i48 = 48;
+    int i49 = 49;
+    int i50 = 50;
+    int i51 = 51;
+    int i52 = 52;
+    int i53 = 53;
+    int i54 = 54;
+    int i55 = 55;
+    int i56 = 56;
+    int i57 = 57;
+    int i58 = 58;
+    int i59 = 59;
+    int i60 = 60;
+    int i61 = 61;
+    int i62 = 62;
+    int i63 = 63;
+    int i64 = 64;
+    int i65 = 65;
+    int i66 = 66;
+    int i67 = 67;
+    int i68 = 68;
+    int i69 = 69;
+    int i70 = 70;
+    int i71 = 71;
+    int i72 = 72;
+    int i73 = 73;
+    int i74 = 74;
+    int i75 = 75;
+    int i76 = 76;
+    int i77 = 77;
+    int i78 = 78;
+    int i79 = 79;
+    int i80 = 80;
+    int i81 = 81;
+    int i82 = 82;
+    int i83 = 83;
+    int i84 = 84;
+    int i85 = 85;
+    int i86 = 86;
+    int i87 = 87;
+    int i88 = 88;
+    int i89 = 89;
+    int i90 = 90;
+    int i91 = 91;
+    int i92 = 92;
+    int i93 = 93;
+    int i94 = 94;
+    int i95 = 95;
+    int i96 = 96;
+    int i97 = 97;
+    int i98 = 98;
+    int i99 = 99;
+    int i100 = 100;
+    int i101 = 101;
+    int i102 = 102;
+    int i103 = 103;
+    int i104 = 104;
+    int i105 = 105;
+    int i106 = 106;
+    int i107 = 107;
+    int i108 = 108;
+    int i109 = 109;
+    int i110 = 110;
+    int i111 = 111;
+    int i112 = 112;
+    int i113 = 113;
+    int i114 = 114;
+    int i115 = 115;
+    int i116 = 116;
+    int i117 = 117;
+    int i118 = 118;
+    int i119 = 119;
+    int i120 = 120;
+    int i121 = 121;
+    int i122 = 122;
+    int i123 = 123;
+    int i124 = 124;
+    int i125 = 125;
+    int i126 = 126;
+    int i127 = 127;
+    int i128 = 128;
+    int i129 = 129;
+    int i130 = 130;
+    int i131 = 131;
+    int i132 = 132;
+    int i133 = 133;
+    int i134 = 134;
+    int i135 = 135;
+    int i136 = 136;
+    int i137 = 137;
+    int i138 = 138;
+    int i139 = 139;
+    int i140 = 140;
+    int i141 = 141;
+    int i142 = 142;
+    int i143 = 143;
+    int i144 = 144;
+    int i145 = 145;
+    int i146 = 146;
+    int i147 = 147;
+    int i148 = 148;
+    int i149 = 149;
+    int i150 = 150;
+    int i151 = 151;
+    int i152 = 152;
+    int i153 = 153;
+    int i154 = 154;
+    int i155 = 155;
+    int i156 = 156;
+    int i157 = 157;
+    int i158 = 158;
+    int i159 = 159;
+    int i160 = 160;
+    int i161 = 161;
+    int i162 = 162;
+    int i163 = 163;
+    int i164 = 164;
+    int i165 = 165;
+    int i166 = 166;
+    int i167 = 167;
+    int i168 = 168;
+    int i169 = 169;
+    int i170 = 170;
+    int i171 = 171;
+    int i172 = 172;
+    int i173 = 173;
+    int i174 = 174;
+    int i175 = 175;
+    int i176 = 176;
+    int i177 = 177;
+    int i178 = 178;
+    int i179 = 179;
+    int i180 = 180;
+    int i181 = 181;
+    int i182 = 182;
+    int i183 = 183;
+    int i184 = 184;
+    int i185 = 185;
+    int i186 = 186;
+    int i187 = 187;
+    int i188 = 188;
+    int i189 = 189;
+    int i190 = 190;
+    int i191 = 191;
+    int i192 = 192;
+    int i193 = 193;
+    int i194 = 194;
+    int i195 = 195;
+    int i196 = 196;
+    int i197 = 197;
+    int i198 = 198;
+    int i199 = 199;
+    int i200 = 200;
+    int i201 = 201;
+    int i202 = 202;
+    int i203 = 203;
+    int i204 = 204;
+    int i205 = 205;
+    int i206 = 206;
+    int i207 = 207;
+    int i208 = 208;
+    int i209 = 209;
+    int i210 = 210;
+    int i211 = 211;
+    int i212 = 212;
+    int i213 = 213;
+    int i214 = 214;
+    int i215 = 215;
+    int i216 = 216;
+    int i217 = 217;
+    int i218 = 218;
+    int i219 = 219;
+    int i220 = 220;
+    int i221 = 221;
+    int i222 = 222;
+    int i223 = 223;
+    int i224 = 224;
+    int i225 = 225;
+    int i226 = 226;
+    int i227 = 227;
+    int i228 = 228;
+    int i229 = 229;
+    int i230 = 230;
+    int i231 = 231;
+    int i232 = 232;
+    int i233 = 233;
+    int i234 = 234;
+    int i235 = 235;
+    int i236 = 236;
+    int i237 = 237;
+    int i238 = 238;
+    int i239 = 239;
+    int i240 = 240;
+    int i241 = 241;
+    int i242 = 242;
+    int i243 = 243;
+    int i244 = 244;
+    int i245 = 245;
+    int i246 = 246;
+    int i247 = 247;
+    int i248 = 248;
+    int i249 = 249;
+    int i250 = 250;
+    int i251 = 251;
+    int i252 = 252;
+    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);
+  }
+}
diff --git a/regression/cbmc-java/lots_of_local_variables/test.desc b/regression/cbmc-java/lots_of_local_variables/test.desc
new file mode 100644
index 00000000000..eaa7d76f397
--- /dev/null
+++ b/regression/cbmc-java/lots_of_local_variables/test.desc
@@ -0,0 +1,6 @@
+CORE
+TooManyLocals.class
+--function TooManyLocals.test
+VERIFICATION SUCCESSFUL
+\[java::TooManyLocals\.test:\(\)V\.assertion\.1\] .*: SUCCESS
+EXIT=0
diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp
index edb251a0fa9..85c63e263b5 100644
--- a/src/java_bytecode/java_bytecode_parser.cpp
+++ b/src/java_bytecode/java_bytecode_parser.cpp
@@ -711,6 +711,13 @@ void java_bytecode_parsert::rbytecode(
       wide_instruction=true;
       address++;
       bytecode=read_u1();
+      // The only valid instructions following a wide byte are
+      // [ifald]load, [ifald]store, ret and iinc
+      // All of these have either format of v, or V
+      INVARIANT(
+        bytecodes[bytecode].format == 'v' || bytecodes[bytecode].format == 'V',
+        "Unexpected wide instruction: " +
+          id2string(bytecodes[bytecode].mnemonic));
     }
 
     instructions.push_back(instructiont());
@@ -749,7 +756,6 @@ void java_bytecode_parsert::rbytecode(
         instruction.args.push_back(from_integer(c, signedbv_typet(8)));
       }
       address+=1;
-
       break;
 
     case 'o': // two byte branch offset, signed
@@ -776,10 +782,20 @@ void java_bytecode_parsert::rbytecode(
 
     case 'v': // local variable index (one byte)
       {
-        u1 v=read_u1();
-        instruction.args.push_back(from_integer(v, unsignedbv_typet(8)));
+        if(wide_instruction)
+        {
+          u2 v = read_u2();
+          instruction.args.push_back(from_integer(v, unsignedbv_typet(16)));
+          address += 2;
+        }
+        else
+        {
+          u1 v = read_u1();
+          instruction.args.push_back(from_integer(v, unsignedbv_typet(8)));
+          address += 1;
+        }
       }
-      address+=1;
+
       break;
 
     case 'V':