|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Macros | |
| #define | new_ast new_solver_ast<btor_smt_ast> |
Functions | |
| void | error_handler (const char *msg) |
| smt_solver_baset * | create_new_boolector_solver (const optionst &options, const namespacet &ns, tuple_iface **tuple_api, array_iface **array_api, fp_convt **fp_api) |
| #define new_ast new_solver_ast<btor_smt_ast> |
| smt_solver_baset * create_new_boolector_solver | ( | const optionst & | options, |
| const namespacet & | ns, | ||
| tuple_iface ** | tuple_api, | ||
| array_iface ** | array_api, | ||
| fp_convt ** | fp_api ) |
| void error_handler | ( | const char * | msg | ) |