Skip to content

Commit 1210a32

Browse files
Natasha Yogananda Jeppudanielsn
Natasha Yogananda Jeppu
authored andcommitted
Modify boolbvt and bv_pointerst to incorporate get_array_constraints boolean option used in arrayst class
Add an additional boolean argument to the class constrcutor to propagate the setting of parse option --show-array-constraints to true to the arrayst class. The entry point for this is in the default invocation of solver factory. clang format solver_factory and bv_pointers
1 parent 1c3395a commit 1210a32

File tree

2 files changed

+6
-4
lines changed

2 files changed

+6
-4
lines changed

src/goto-checker/solver_factory.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -219,9 +219,10 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
219219
solver->set_prop(make_satcheck_prop<satcheckt>(message_handler, options));
220220
}
221221

222-
bool get_array_constraints = options.get_bool_option("show-array-constraints");
223-
auto bv_pointers =
224-
util_make_unique<bv_pointerst>(ns, solver->prop(), message_handler, get_array_constraints);
222+
bool get_array_constraints =
223+
options.get_bool_option("show-array-constraints");
224+
auto bv_pointers = util_make_unique<bv_pointerst>(
225+
ns, solver->prop(), message_handler, get_array_constraints);
225226

226227
if(options.get_option("arrays-uf") == "never")
227228
bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_NONE;

src/solvers/flattening/bv_pointers.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,8 @@ bv_pointerst::bv_pointerst(
8484
propt &_prop,
8585
message_handlert &message_handler,
8686
bool get_array_constraints)
87-
: boolbvt(_ns, _prop, message_handler, get_array_constraints), pointer_logic(_ns)
87+
: boolbvt(_ns, _prop, message_handler, get_array_constraints),
88+
pointer_logic(_ns)
8889
{
8990
object_bits=config.bv_encoding.object_bits;
9091
std::size_t pointer_width = boolbv_width(pointer_type(empty_typet()));

0 commit comments

Comments
 (0)