14 #ifndef CPROVER_GOTO_SYMEX_BUILD_GOTO_TRACE_H
15 #define CPROVER_GOTO_SYMEX_BUILD_GOTO_TRACE_H
40 symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep,
45 typedef std::function<bool(
46 symex_target_equationt::SSA_stepst::const_iterator,
void build_goto_trace(const symex_target_equationt &target, const decision_proceduret &decision_procedure, const namespacet &ns, goto_tracet &goto_trace)
Build a trace by going through the steps of target and stopping at the first failing assertion.
std::function< bool(symex_target_equationt::SSA_stepst::const_iterator, const decision_proceduret &)> ssa_step_predicatet
An interface for a decision procedure for satisfiability problems.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Generate Equation using Symbolic Execution.