conjunctive clauses are discarded

[n-osborne]

Currently, we look at the head of a clause (the first node in the term AST) to decide whether it contains the infomration we are looking for. This will disqualify any clause constructed as a conjunction.

For example, the following file:

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

val make : int -> 'a -> 'a t
(*@ t = make i a
    ensures t.contents = List.init i (fun j -> a) *)

val set : 'a t -> int -> 'a -> unit
(*@ set t i a
    modifies t.contents
    ensures true /\ t.contents = List.mapi (fun j x -> if j = (i : integer) then a else x) (old t.contents) *)

will raise:

$ ortac qcheck-stm file.mli "make 42 0" "int t" -o /dev/null
File "file.mli", line 10, characters 13-23:
10 |     modifies t.contents
                  ^^^^^^^^^^
Warning: Skipping set: model contents is declared as modified by the function
         but no translatable ensures clause was found.

This is a limitation for the generation of next_state and init_state that should be easy to overcome.