// example from page 104
// not provable when chosing intRules:javaSemantics in Options | "Taclet Options Default"
// in the KeY prover

\javaSource "source/formulas";

\functions{
  int g;
}

\programVariables { 
  int c;
}

\problem {

{ArrayList.v:=g}\<{ ArrayList al=new ArrayList(); 
                    int arg=ArrayList.v; 
                    int j; 
                    j=al.inc(arg)@ArrayList; 
                    ArrayList.v=j;}\>ArrayList.v=g+1

}