Inheritance diagram for bv_refinementt::infot:

Collaboration diagram for bv_refinementt::infot:

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

Detailed Description

Definition at line 33 of file bv_refinement.h.

Member Data Documentation

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.

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

/home/runner/work/cbmc-documentation/cbmc-documentation/src/solvers/refinement/bv_refinement.h