cprover
k_induction.cpp File Reference

k-induction More...

#include "k_induction.h"
#include <util/std_expr.h>
#include <analyses/natural_loops.h>
#include <analyses/local_may_alias.h>
#include <goto-programs/remove_skip.h>
#include "unwind.h"
#include "loop_utils.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_functionst &goto_functions, 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_functionst goto_functions,
bool  base_case,
bool  step_case,
unsigned  k 
)