10 #ifndef CPROVER_SOLVERS_FLATTENING_FLATTEN_BYTE_OPERATORS_H 11 #define CPROVER_SOLVERS_FLATTENING_FLATTEN_BYTE_OPERATORS_H 32 #endif // CPROVER_SOLVERS_FLATTENING_FLATTEN_BYTE_OPERATORS_H exprt flatten_byte_operators(const exprt &src, const namespacet &ns)
exprt flatten_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
rewrite byte extraction from an array to byte extraction from a concatenation of array index expressi...
bool has_byte_operator(const exprt &src)
Base class for all expressions.
exprt flatten_byte_update(const byte_update_exprt &src, const namespacet &ns)