Module Lib.ReservedIds

Reserved identifiers.

val abs_ident_string : string

New variables from abstraction.

val oracle_ident_string : string

New oracle input.

val instance_ident_string : string

Unique identifier for node instance.

val init_flag_ident_string : string

First instant flag.

val all_req_ident_string : string

Observer for contract requirements.

val all_ens_ident_string : string

Observer for contract ensures.

val inst_ident_string : string

New variables from node instance.

val eq_vars_ident_string : string

Observer for variable equivalence

val init_uf_string : string

Initial predicate.

val trans_uf_string : string

Transition relation.

val index_ident_string : string

New clock initialization flag.

val init_flag_string : string

Init flag string.

val depth_input_string : string

Abstraction depth input string.

val max_depth_input_string : string

Abstraction depth input string.

val function_of_inputs : string

Suffix used for the name of the function encoding functional systems.

val undefined_call : string

Value of a recursive call whose termination checks fail, in the SMT-level definition of a recursive function

val function_definition : string

Definition of an output of a function that is neither recursive nor imported, in the SMT-level definition of a recursive function

val reserved_strings : string list

All reserved identifiers.