Lazy methods: fault in static initializer if a static method is called

regression/cbmc-java/lazyloading5/test.desc

@@ -0,0 +1,6 @@
+CORE
+test.class
+--lazy-methods --function test.main
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL

regression/cbmc-java/lazyloading5/test.java

@@ -0,0 +1,21 @@
+
+public class test {
+
+  public static void main() {
+
+    assert(other.getx()==1);
+
+  }
+
+}
+
+class other {
+
+  public static int x;
+  public static int getx() { return x; }
+
+  static {
+    x=1;
+  }
+
+}

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1418,7 +1418,11 @@ codet java_bytecode_convert_methodt::convert_instructions(
         // static binding
         call.function()=symbol_exprt(arg0.get(ID_identifier), arg0.type());
         if(lazy_methods)
+        {
           lazy_methods->add_needed_method(arg0.get(ID_identifier));
+          // Calling a static method causes static initialization:
+          lazy_methods->add_needed_class(arg0.get(ID_C_class));
+        }
       }
 
       call.function().add_source_location()=loc;