|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
#include <cassert>#include <goto-symex/scheduler/execution_state.h>#include <goto-symex/engine/goto_symex.h>#include <goto-symex/scheduler/reachability_tree.h>#include <string>#include <util/arith/arith_tools.h>#include <util/expr/base_type.h>#include <util/lang/c_types.h>#include <util/symtab/context.h>#include <util/expr/expr_util.h>#include <irep2/irep2.h>#include <util/message/message.h>#include <util/irep/migrate.h>#include <util/irep/std_types.h>#include <util/symtab/symbol.h>