ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
bitwuzla_conv.cpp File Reference
#include <bitwuzla_conv.h>
#include <cstdio>
#include <sstream>
Include dependency graph for bitwuzla_conv.cpp:

Macros

#define new_ast   new_solver_ast<bitw_smt_ast>

Functions

smt_solver_baset * create_new_bitwuzla_solver (const optionst &options, const namespacet &ns, tuple_iface **tuple_api, array_iface **array_api, fp_convt **fp_api)

Macro Definition Documentation

◆ new_ast

#define new_ast   new_solver_ast<bitw_smt_ast>

Function Documentation

◆ create_new_bitwuzla_solver()

smt_solver_baset * create_new_bitwuzla_solver ( const optionst & options,
const namespacet & ns,
tuple_iface ** tuple_api,
array_iface ** array_api,
fp_convt ** fp_api )