diff --git a/regression/cbmc-java/synchronized/Sync.class b/regression/cbmc-java/synchronized/Sync.class
new file mode 100644
index 00000000000..0c493d5eea9
Binary files /dev/null and b/regression/cbmc-java/synchronized/Sync.class differ
diff --git a/regression/cbmc-java/synchronized/Sync.java b/regression/cbmc-java/synchronized/Sync.java
new file mode 100644
index 00000000000..2f8f91cc2ae
--- /dev/null
+++ b/regression/cbmc-java/synchronized/Sync.java
@@ -0,0 +1,11 @@
+public class Sync {
+  public static void main(String[] args) {
+    final Object o = null;
+    try {
+      synchronized (o) {}
+      assert false;
+    } catch (NullPointerException e) {
+      return;
+    }
+  }
+}
diff --git a/regression/cbmc-java/synchronized/test.desc b/regression/cbmc-java/synchronized/test.desc
new file mode 100644
index 00000000000..7155ff81375
--- /dev/null
+++ b/regression/cbmc-java/synchronized/test.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+Sync.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+See #1236 for details of this test.