Ошибки при запуске OpenJML с двумя классами

Question

Я проверил оба следующих фрагмента кода с помощью OpenJML:

public class Customer {

    /*@ public invariant this.customerID != 0; */
    /*@ public invariant this.customerID >= -1; */  
    /*@ spec_public */ private int customerID;  
    /*@
    @ public normal_behavior
    @ requires customerID != 0;
    @ requires customerID >= -1;

    @*/
    public Customer(int customerID) {
        this.customerID = customerID;
    }

    /*@
    @ public normal_behavior 
    @ requires true;
    @*/
    public int getId() {
        return customerID;
    }   

    /*@
    @ also
    @ public normal_behavior // Generated by Daikon
    @ requires true;
    @*/
    public String toString() {
        return "I am customer with ID " + customerID + ".";
    }
}

public class Order {

    /*@ public invariant this.orderID != 0; */
    /*@ public invariant this.orderID >= -1; */
    /*@ spec_public */ private int orderID;

    /*@
    @ public normal_behavior 
    @ requires orderID != 0;
    @ requires orderID >= -1;
    @*/
    public Order(int orderID) {
        this.orderID = orderID;
    }

    /*@
    @ public normal_behavior 
    @ requires true;
    @*/
    public int getOrderID() {
        return orderID;     
    }   
}

и я не получаю предупреждений. Я запустил java -jar openjml.jar -esc examples/Customer.java и java -jar openjml.jar -esc examples/Order.java. Примеры папок содержат файлы Customer.java и Order.java.

Однако, когда я изменяю Customer.java, чтобы включить в него объект Order, например:

public class Customer {

    /*@ public invariant this.customerID != 0; */
    /*@ public invariant this.customerID >= -1; */
    /*@ public invariant this.order != null; */
    /*@ public invariant this.order.orderID != 0; */
    /*@ public invariant this.order.orderID >= -1; */
    /*@ spec_public */ private int customerID;
    /*@ spec_public */ private Order order;

    /*@
    @ public normal_behavior 
    @ requires customerID != 0;
    @ requires customerID >= -1;
    @ ensures this.order.orderID == -1;
    @*/
    public Customer(int customerID) {
        this.customerID = customerID;
        this.order = new Order(-1);
    }

    /*@
    @ public normal_behavior
    @ requires true;
    @*/
    public int getId() {
        return customerID;
    }   

    /*@
    @ public normal_behavior 
    @ ensures this.customerID == \old(this.customerID);
    @ ensures this.order == \result;
    @ ensures this.order.orderID == \result.orderID;
    @ ensures \result == \old(this.order);
    @ ensures \result.orderID == \old(this.order.orderID);
    @ ensures \result != null;
    @*/
    public Order getOrder() {
        return order;
    }

    /*@
    @ public normal_behavior 
    @ requires this.order.orderID == -1;
    @ requires o != null;
    @ requires this.order != null ==> o != null;
    @ requires this.order.orderID < o.orderID;
    @ ensures this.customerID == \old(this.customerID);
    @ ensures this.order == \old(o);
    @ ensures this.order.orderID == o.orderID;
    @ ensures o.orderID == \old(o.orderID);
    @ ensures this.order != null ==> \old(this.order) != null;
    @ ensures o.orderID > \old(this.order.orderID);
    @*/
    public void setOrder(Order o){
        this.order = o;
    }

    /*@
    @ also
    @ public normal_behavior 
    @ requires true;
    @*/
    public String toString() {
        return "I am customer with ID " + customerID + ".";
    }
}

после выполнения примеров java -jar openjml.jar -esc -dir я получаю следующие предупреждения:

examples/Customer.java:17: warning: The prover cannot establish an assertion (InvariantExit: examples/Customer.java:4: ) in method Customer
    public Customer(int customerID) {
           ^
examples/Customer.java:4: warning: Associated declaration: examples/Customer.java:17: 
    /*@ public invariant this.customerID >= -1; */
               ^

examples/Customer.java:17: warning: The prover cannot establish an assertion (InvariantExit: examples/Customer.java:3: ) in method Customer
    public Customer(int customerID) {
           ^
examples/Customer.java:3: warning: Associated declaration: examples/Customer.java:17: 
    /*@ public invariant this.customerID != 0; */
               ^

examples/Customer.java:17: warning: The prover cannot establish an assertion (Postcondition: examples/Customer.java:15: ) in method Customer
    public Customer(int customerID) {
           ^
examples/Customer.java:15: warning: Associated declaration: examples/Customer.java:17: 
    @ ensures this.order.orderID == -1;
      ^
6 warnings

Я не могу понять, почему это происходит.