k-induction More...
#include "k_induction.h"#include <analyses/natural_loops.h>#include <analyses/local_may_alias.h>#include <goto-programs/remove_skip.h>#include "havoc_utils.h"#include "loop_utils.h"#include "unwind.h"
Include dependency graph for k_induction.cpp:Go to the source code of this file.
Classes | |
| class | k_inductiont |
Functions | |
| void | k_induction (goto_modelt &goto_model, bool base_case, bool step_case, unsigned k) |
Detailed Description
k-induction
Definition in file k_induction.cpp.
Function Documentation
◆ k_induction()
| void k_induction | ( | goto_modelt & | goto_model, |
| bool | base_case, | ||
| bool | step_case, | ||
| unsigned | k | ||
| ) |
Definition at line 168 of file k_induction.cpp.
