docs/api/goto__k__induction_8h_source.html

#ifndef GOTO_PROGRAMS_GOTO_K_INDUCTION_H_

#define GOTO_PROGRAMS_GOTO_K_INDUCTION_H_


#include <goto-programs/goto_functions.h>

#include <util/symtab/namespace.h>


bool goto_k_induction(

  goto_functionst &goto_functions,

  const namespacet &ns,

  bool continue_past_failed_assertions);


#endif /* GOTO_PROGRAMS_GOTO_K_INDUCTION_H_ */

goto_functionst
Definition goto_functions.h:56

namespacet
Definition namespace.h:10

goto_functions.h

goto_k_induction
bool goto_k_induction(goto_functionst &goto_functions, const namespacet &ns, bool continue_past_failed_assertions)
Per-loop k-induction transformation: havoc each loop's modified variables and inject an ASSUME of the...
Definition goto_k_induction.cpp:1971

namespace.h