#407 java.lang.StackOverflowError

[Dr Ian Bayley]

I get a java.lang.StackOverflowError when ESCing, with the Z3 tool, at the command line the following program:

import java.util.ArrayList;
public class JMLArrayListExample {
public ArrayList<String> elements;

public JMLArrayListExample () {
    elements = new ArrayList<String>();
}

//@ ensures (elements.contains(s));
public void add(String s){
    elements.add(s);

}

public static void main (String[] args){
    System.out.println("wait");
    JMLArrayListExample jale = new JMLArrayListExample();
    jale.add("hello");

}

}

[David Cok]

Problem reproduced and now in the OpenJML test suite. Not yet fixed.