24 std::size_t unique_id,
25 bool is_dynamic_object)
const
29 INVARIANT(id_sort,
"Object identifiers are expected to have bit vector sort");
30 const auto bit_vector_of_id =
A function generated from a command.
static const smt_function_application_termt::factoryt< equalt > equal
Stores identifiers in unescaped and unquoted form.
static smt_declare_function_commandt make_is_dynamic_object_function_declaration()
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
make_applicationt make_application
smt_declare_function_commandt declaration
The command for declaring the is_dynamic_object function.
smt_commandt make_definition(std::size_t unique_id, bool is_dynamic_object) const
Makes the command to define the resulting is_dynamic_object status for calls to the is_dynamic_object...