12 #ifndef CPROVER_GOTO_SYMEX_SLICE_H 13 #define CPROVER_GOTO_SYMEX_SLICE_H 28 const std::list<exprt> &expressions);
38 #endif // CPROVER_GOTO_SYMEX_SLICE_H Generate Equation using Symbolic Execution.
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
std::unordered_set< irep_idt > symbol_sett
void simple_slice(symex_target_equationt &equation)
void collect_open_variables(const symex_target_equationt &equation, symbol_sett &open_variables)
Collect the open variables, i.e.
void slice(symex_target_equationt &equation)