CBMC
|
#include <bv_refinement.h>
Public Attributes | |
const namespacet * | ns =nullptr |
propt * | prop =nullptr |
message_handlert * | message_handler = nullptr |
Public Attributes inherited from bv_refinementt::configt | |
bool | output_xml = false |
unsigned | max_node_refinement =5 |
Max number of times we refine a formula node. More... | |
bool | refine_arrays =true |
Enable array refinement. More... | |
bool | refine_arithmetic =true |
Enable arithmetic refinement. More... | |
Definition at line 33 of file bv_refinement.h.
message_handlert* bv_refinementt::infot::message_handler = nullptr |
Definition at line 37 of file bv_refinement.h.
const namespacet* bv_refinementt::infot::ns =nullptr |
Definition at line 35 of file bv_refinement.h.
propt* bv_refinementt::infot::prop =nullptr |
Definition at line 36 of file bv_refinement.h.