Error on synchronization on objects in Java

[mgudemann]

This example fails with unexpected statement: monitorenter

public class monitorenter1
{
  public boolean doIt(boolean b)
  {
    boolean a;
    synchronized(this) {
      a = !b;
    }
    return a;
  }
  public void test()
  {
    assert(doIt(false));
  }
}

the critical section is enclosed between monitorenter and monitorexit in the bytecode.

[kroening]

Added as regression/cbmc-java/monitorenter1

[peterschrammel]

fixed