Detection of rsymbol that corresponds to a constant
Currently a declaration of the form
val constant x : int
is transformed into
let constant x : int { ensures result = x } = fun -> any int
This particular encoding should be taken into account both in extraction and execution.
Feature wish : provide a new OCaml function that, given a rsymbol rs
, and possibly the environment to access to its declaration, tells whether this rsymbol is a regular function or an encoding of a constant.