import liquidjava.specification.Ghost;
import liquidjava.specification.Refinement;
import liquidjava.specification.StateRefinement;

public class Outer {
    @Ghost("int size")
    static class Bag {
        @StateRefinement(to = "size(this) == 0")
        public Bag() {}

        @StateRefinement(to = "size(this) == size(old(this)) + 1")
        public void add() {}

        @StateRefinement(from = "size(this) > 0")
        public void remove() {}
    }

    static void ok() {
        Bag b = new Bag();
        b.add();
        b.remove();
    }
}

Error: Sort mismatch at argument #1 for function (declare-fun Outer$Bag.size (Outer.Bag) Int) supplied sort is Outer$Bag
 9 |         public Bag() {}
10 | 
11 |         @StateRefinement(to = "size(this) == size(old(this)) + 1")
   |                                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
12 |         public void add() {}
13 | 

Error: Sort mismatch at argument #1 for function (declare-fun Outer$Bag.size (Outer.Bag) Int) supplied sort is Outer$Bag
12 |         public void add() {}
13 | 
14 |         @StateRefinement(from = "size(this) > 0")
   |                                  ^^^^^^^^^^^^^^
15 |         public void remove() {}
16 |     }