class Test {
    /*@ public normal_behavior
      @   requires s != null;
      @   requires s.equals("yes") || s.equals("no");
      @   ensures s.equals("yes") ==> \result == 1;
      @   ensures s.equals("no")  ==> \result == 0;
      @   assignable \strictly_nothing;
      @*/
    public int broken(String s) {
        if (s.equals("yes"))
          return 1;
        if (s.equals("no"))
          return 0;
        return -1;
    }
    
    /*@ public normal_behavior
      @   requires s != null;
      @   requires s.equals("yes") || s.equals("no");
      @   ensures s.equals("yes") ==> \result == 1;
      @   ensures s.equals("no")  ==> \result == 0;
      @   assignable \strictly_nothing;
      @*/
    public int works(String s) {
        // Have literals in the code so queries can evaluate
        String s1 = "yes";
        s1 = "no";
        if (s.equals("yes"))
          return 1;
        if (s.equals("no"))
          return 0;
        return -1;
    }
}