cprover
|
#include <bv_refinement.h>
Public Attributes | |
const namespacet * | ns =nullptr |
propt * | prop =nullptr |
![]() | |
ui_message_handlert::uit | ui =ui_message_handlert::uit::PLAIN |
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 35 of file bv_refinement.h.
const namespacet* bv_refinementt::infot::ns =nullptr |
Definition at line 37 of file bv_refinement.h.
Referenced by cbmc_solverst::get_bv_refinement(), cbmc_solverst::get_string_refinement(), and validate().
propt* bv_refinementt::infot::prop =nullptr |
Definition at line 38 of file bv_refinement.h.
Referenced by cbmc_solverst::get_bv_refinement(), cbmc_solverst::get_string_refinement(), and validate().