ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
remove_library_assertions.h
Go to the documentation of this file.
1#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_LIBRARY_ASSERTIONS_H
2#define CPROVER_GOTO_PROGRAMS_REMOVE_LIBRARY_ASSERTIONS_H
3
4#include <goto-programs/goto_functions.h>
5
12void remove_library_assertions(goto_functionst &goto_functions);
13
14#endif
goto_functionst
Definition goto_functions.h:56
goto_functions.h
remove_library_assertions
void remove_library_assertions(goto_functionst &goto_functions)
Drop every assertion stated by ESBMC's own operational models, i.e.
Definition remove_library_assertions.cpp:6