14 #ifndef CPROVER_GOTO_SYMEX_BUILD_GOTO_TRACE_H 15 #define CPROVER_GOTO_SYMEX_BUILD_GOTO_TRACE_H 30 symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep,
35 typedef std::function<
36 bool(symex_target_equationt::SSA_stepst::const_iterator,
const prop_convt &)>
47 #endif // CPROVER_GOTO_SYMEX_BUILD_GOTO_TRACE_H Generate Equation using Symbolic Execution.
std::function< bool(symex_target_equationt::SSA_stepst::const_iterator, const prop_convt &)> ssa_step_predicatet
void build_goto_trace(const symex_target_equationt &target, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)