qcheck-stm is a bit too leniant on some clauses

[shym]

Given the following source:

type 'a t
(*@ mutable model value : 'a list *)
val make : 'a -> 'a t
(*@ t = make a
    requires true
    ensures t.value = t.value *)

ortac qcheck-stm foo.mli "make 42" "int t" will accept to generate the following broken code:

let init_state = let a_1 = 42 in { value = (t_1.value) }

This might be making the case for a call to subst_term with None for both old and new.