assertion failed about constant
Closed this issue · 0 comments
n-osborne commented
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