ocaml-gospel/ortac

assertion failed about constant

Closed this issue · 0 comments

Given the following interface:

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

val make : unit -> 'a t
(*@ t = make ()
    ensures t.contents = [] *)

val constant : unit
(*@ constant *)

ortac qcheck-stm file.mli "make ()" "char t" will complain about an internal error.

ortac: internal error, uncaught exception:
       File "plugins/qcheck-stm/src/ir_of_gospel.ml", line 71, characters 2-8: Assertion failed