diffblue · thk123 · Aug 14, 2017 · Aug 11, 2017
diff --git a/regression/cbmc-java/synchronized/Sync.class b/regression/cbmc-java/synchronized/Sync.class
diff --git a/regression/cbmc-java/synchronized/Sync.java 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
@@ -0,0 +1,10 @@
+KNOWNBUG
+Sync.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+See #1236 for details of this test.