|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
#include <solvers/smt/smt_solver.h>#include <solvers/smt/tuple/smt_tuple_array_ast.h>#include <solvers/smt/tuple/smt_tuple_sym.h>#include <solvers/smt/tuple/smt_tuple_sym_ast.h>#include <sstream>#include <util/expr/base_type.h>#include <util/lang/c_types.h>