`Old` field use in New Object (just after constructor)

[CatarinaGamboa]

It seems that the fields are always appended with the predicate field(this) == field(old(this)) if there is no mention to the field in a predicate. However, this should not happen in the constructor, otherwise there will be an error in trying to access the old of something new. We can maybe use some default value (which is what happens if there is no class constructor)

Here is an example of the error happening:

@StateSet({"leaf", "onlyRight", "onlyLeft", "both"})
public class Tree {
    private int val;

    @StateRefinement(to = "leaf(this)")
    public Tree(){}

    @StateRefinement(to="val(this)==x")
    public void addVal(int x) {val = x;}

    public static void main(String[] args) {
        Tree a = new Tree();
        a.addVal(10);
        }
}

Error Message:

----------------------------VC--------------------------------
∀#a_6:Tree,           (leaf(#a_6)) && val(#a_6) == val(old(#a_6))  => 
                     (leaf(#a_6))

SMT subtyping:true && (leaf(#a_6)) && val(#a_6) == val(old(#a_6)) <: true)
--------------------------------------------------------------
Function old not found

[CatarinaGamboa]

Duplicate of #32