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.

Author: Natasha Yogananda Jeppu

src/goto-checker/solver_factory.cpp

@@ -219,8 +219,9 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
     solver->set_prop(make_satcheck_prop<satcheckt>(message_handler, options));
   }
 
+  bool get_array_constraints = options.get_bool_option("show-array-constraints");
   auto bv_pointers =
-    util_make_unique<bv_pointerst>(ns, solver->prop(), message_handler);
+    util_make_unique<bv_pointerst>(ns, solver->prop(), message_handler, get_array_constraints);
 
   if(options.get_option("arrays-uf") == "never")
     bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_NONE;

src/solvers/flattening/boolbv.h

@@ -37,8 +37,9 @@ class boolbvt:public arrayst
   boolbvt(
     const namespacet &_ns,
     propt &_prop,
-    message_handlert &message_handler)
-    : arrayst(_ns, _prop, message_handler),
+    message_handlert &message_handler,
+    bool get_array_constraints = false)
+    : arrayst(_ns, _prop, message_handler, get_array_constraints),
       unbounded_array(unbounded_arrayt::U_NONE),
       boolbv_width(_ns),
       bv_utils(_prop),

src/solvers/flattening/bv_pointers.cpp

@@ -82,8 +82,9 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
 bv_pointerst::bv_pointerst(
   const namespacet &_ns,
   propt &_prop,
-  message_handlert &message_handler)
-  : boolbvt(_ns, _prop, message_handler), pointer_logic(_ns)
+  message_handlert &message_handler,
+  bool get_array_constraints)
+  : boolbvt(_ns, _prop, message_handler, get_array_constraints), pointer_logic(_ns)
 {
   object_bits=config.bv_encoding.object_bits;
   std::size_t pointer_width = boolbv_width(pointer_type(empty_typet()));

src/solvers/flattening/bv_pointers.h

@@ -20,7 +20,8 @@ class bv_pointerst:public boolbvt
   bv_pointerst(
     const namespacet &_ns,
     propt &_prop,
-    message_handlert &message_handler);
+    message_handlert &message_handler,
+    bool get_array_constraints = false);
 
   void post_process() override;