qcheck-stm generates `next_state` function pattern matching on out of scope returned value

[n-osborne]

In the following example, which gospel typecheck, we mention the returned value in the postcondition describing the new state.

type 'a t
(*@ mutable model contents : 'a sequence *)

val create : unit -> 'a t
(*@ q = create ()
    ensures q.contents = Sequence.empty *)

val pop_opt : 'a t -> 'a option
(*@ o = pop_opt q
    modifies q.contents
    ensures q.contents = match o with
                          | None -> Sequence.empty
                          | Some _ -> Sequence.tl (old q.contents) *)

$ ortac qcheck-stm issue.mli "create ()" "int t"

will happily generate a next-state function pattern matching on the returned value that is not in scope:

    let next_state cmd__002_ state__003_ =
      match cmd__002_ with
      | Pop_opt ->
          {
            contents =
              ((try
                  match o with
                  | None -> Ortac_runtime.Gospelstdlib.Sequence.empty
                  | Some _ ->
                      Ortac_runtime.Gospelstdlib.Sequence.tl
                        state__003_.contents
                with
                | e ->
                    raise
                      (Ortac_runtime.Partial_function
                         (e,
                           {
                             Ortac_runtime.start =
                               {
                                 pos_fname = "issue.mli";
                                 pos_lnum = 11;
                                 pos_bol = 430;
                                 pos_cnum = 455
                               };
                             Ortac_runtime.stop =
                               {
                                 pos_fname = "issue.mli";
                                 pos_lnum = 13;
                                 pos_bol = 519;
                                 pos_cnum = 585
                               }
                           }))))
          }

[shym]

Good catch! I wonder if we should add a list of prohibited variables to the subst_term function, in order to detect if one of the returned values appears in a term that is a candidate for next_state. Would that make sense? It could be cleaner to just define another function for that very purpose.