diff --git a/regression/cbmc-java/LocalVarTable3/live_range_with_holes.class b/regression/cbmc-java/LocalVarTable3/live_range_with_holes.class
new file mode 100644
index 00000000000..af3f7e4358a
Binary files /dev/null and b/regression/cbmc-java/LocalVarTable3/live_range_with_holes.class differ
diff --git a/regression/cbmc-java/LocalVarTable3/live_range_with_holes.java b/regression/cbmc-java/LocalVarTable3/live_range_with_holes.java
new file mode 100644
index 00000000000..fda6daf9b5a
--- /dev/null
+++ b/regression/cbmc-java/LocalVarTable3/live_range_with_holes.java
@@ -0,0 +1,26 @@
+
+public class live_range_with_holes {
+
+  public static void main(int arg) {
+
+    int x;
+    int y;
+    switch(arg) {
+      case 1:
+        x = 1;
+        y = 1;
+        break;
+      case 2:
+        x = 2;
+        y = 2;
+        break;
+      default:
+        x = 0;
+        y = 0;
+        break;
+    }
+    assert(x >= 0 && x <= 2);
+
+  }
+
+}
diff --git a/regression/cbmc-java/LocalVarTable3/test.desc b/regression/cbmc-java/LocalVarTable3/test.desc
new file mode 100644
index 00000000000..a50e15252db
--- /dev/null
+++ b/regression/cbmc-java/LocalVarTable3/test.desc
@@ -0,0 +1,7 @@
+CORE
+live_range_with_holes.class
+--function live_range_with_holes.main
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
diff --git a/regression/cbmc-java/LocalVarTable4/live_range_exception.class b/regression/cbmc-java/LocalVarTable4/live_range_exception.class
new file mode 100644
index 00000000000..71b1dd48d11
Binary files /dev/null and b/regression/cbmc-java/LocalVarTable4/live_range_exception.class differ
diff --git a/regression/cbmc-java/LocalVarTable4/live_range_exception.java b/regression/cbmc-java/LocalVarTable4/live_range_exception.java
new file mode 100644
index 00000000000..52e5d54070a
--- /dev/null
+++ b/regression/cbmc-java/LocalVarTable4/live_range_exception.java
@@ -0,0 +1,18 @@
+
+public class live_range_exception {
+  public static void main() {
+    int x;
+    int y;
+    try
+    {
+      x = 0;
+      y = 0;
+    }
+    catch(Exception e)
+    {
+      x = 1;
+      y = 1;
+    }
+    assert(x==0 || x==1);
+  }
+}
diff --git a/regression/cbmc-java/LocalVarTable4/test.desc b/regression/cbmc-java/LocalVarTable4/test.desc
new file mode 100644
index 00000000000..bf94c110fcc
--- /dev/null
+++ b/regression/cbmc-java/LocalVarTable4/test.desc
@@ -0,0 +1,7 @@
+CORE
+live_range_exception.class
+--function live_range_exception.main
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--