cprover
bv_refinementt::configt Struct Reference
Inheritance diagram for bv_refinementt::configt:
[legend]

Public Attributes

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...
 

Detailed Description

Definition at line 24 of file bv_refinement.h.

Member Data Documentation

◆ max_node_refinement

unsigned bv_refinementt::configt::max_node_refinement =5

Max number of times we refine a formula node.

Definition at line 28 of file bv_refinement.h.

Referenced by bv_refinementt::check_SAT(), cbmc_solverst::get_bv_refinement(), and cbmc_solverst::get_string_refinement().

◆ refine_arithmetic

bool bv_refinementt::configt::refine_arithmetic =true

◆ refine_arrays

bool bv_refinementt::configt::refine_arrays =true

◆ ui


The documentation for this struct was generated from the following file: