Extract mapst base class from arrayst

src/cprover/bv_pointers_wide.cpp

@@ -155,8 +155,8 @@ bv_pointers_widet::bv_pointers_widet(
   const namespacet &_ns,
   propt &_prop,
   message_handlert &message_handler,
-  bool get_array_constraints)
-  : boolbvt(_ns, _prop, message_handler, get_array_constraints),
+  bool collect_constraint_stats)
+  : boolbvt(_ns, _prop, message_handler, collect_constraint_stats),
     pointer_logic(_ns)
 {
 }

src/cprover/bv_pointers_wide.h

@@ -23,7 +23,7 @@ class bv_pointers_widet : public boolbvt
     const namespacet &,
     propt &,
     message_handlert &,
-    bool get_array_constraints = false);
+    bool collect_constraint_stats = false);
 
   void finish_eager_conversion() override;
 

src/goto-checker/solver_factory.cpp

@@ -356,10 +356,10 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
 {
   auto sat_solver = get_sat_solver(message_handler, options);
 
-  bool get_array_constraints =
+  bool collect_constraint_stats =
     options.get_bool_option("show-array-constraints");
   auto bv_pointers = std::make_unique<bv_pointerst>(
-    ns, *sat_solver, message_handler, get_array_constraints);
+    ns, *sat_solver, message_handler, collect_constraint_stats);
 
   if(options.get_option("arrays-uf") == "never")
     bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_NONE;

src/solvers/Makefile

@@ -140,6 +140,7 @@ SRC = $(BOOLEFORCE_SRC) \
       flattening/bv_utils.cpp \
       flattening/c_bit_field_replacement_type.cpp \
       flattening/equality.cpp \
+      flattening/maps.cpp \
       flattening/pointer_logic.cpp \
       floatbv/float_bv.cpp \
       floatbv/float_utils.cpp \