From 440ea267ac934c18053fcec0295053d018a6b170 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 12 Sep 2022 05:42:32 +0000
Subject: [PATCH 1/3] Use bv_utilst::zeros

This makes code more concise and possibly more efficient.
---
 src/solvers/flattening/boolbv_div.cpp |  3 +--
 src/solvers/flattening/bv_utils.cpp   | 14 +++-----------
 2 files changed, 4 insertions(+), 13 deletions(-)

diff --git a/src/solvers/flattening/boolbv_div.cpp b/src/solvers/flattening/boolbv_div.cpp
index 4d4d1c514af..a1739488aab 100644
--- a/src/solvers/flattening/boolbv_div.cpp
+++ b/src/solvers/flattening/boolbv_div.cpp
@@ -37,8 +37,7 @@ bvt boolbvt::convert_div(const div_exprt &expr)
     std::size_t fraction_bits=
       to_fixedbv_type(expr.type()).get_fraction_bits();
 
-    bvt zeros;
-    zeros.resize(fraction_bits, const_literal(false));
+    bvt zeros = bv_utils.zeros(fraction_bits);
 
     // add fraction_bits least-significant bits
     op0.insert(op0.begin(), zeros.begin(), zeros.end());
diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp
index 0b163b153df..0a9b7d01369 100644
--- a/src/solvers/flattening/bv_utils.cpp
+++ b/src/solvers/flattening/bv_utils.cpp
@@ -715,13 +715,9 @@ bvt bv_utilst::unsigned_multiplier(const bvt &_op0, const bvt &_op1)
   for(std::size_t sum=0; sum<op0.size(); sum++)
     if(op0[sum]!=const_literal(false))
     {
-      bvt tmpop;
-
+      bvt tmpop = zeros(sum);
       tmpop.reserve(op0.size());
 
-      for(std::size_t idx=0; idx<sum; idx++)
-        tmpop.push_back(const_literal(false));
-
       for(std::size_t idx=sum; idx<op0.size(); idx++)
         tmpop.push_back(prop.land(op1[idx-sum], op0[sum]));
 
@@ -746,13 +742,9 @@ bvt bv_utilst::unsigned_multiplier(const bvt &_op0, const bvt &_op1)
   for(std::size_t bit=0; bit<op0.size(); bit++)
     if(op0[bit]!=const_literal(false))
     {
-      bvt pp;
-
-      pp.reserve(op0.size());
-
       // zeros according to weight
-      for(std::size_t idx=0; idx<bit; idx++)
-        pp.push_back(const_literal(false));
+      bvt pp = zeros(bit);
+      pp.reserve(op0.size());
 
       for(std::size_t idx=bit; idx<op0.size(); idx++)
         pp.push_back(prop.land(op1[idx-bit], op0[bit]));

From 320ab53043cd8e062158c5506b910b607f6239a0 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 12 Sep 2022 05:43:22 +0000
Subject: [PATCH 2/3] Rename variable for clarity

This bit vector is not necessarily filled with zeros. Also, use
`pop_back` to avoid an iterator dance.
---
 src/solvers/flattening/bv_utils.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp
index 0a9b7d01369..425f2ba40e1 100644
--- a/src/solvers/flattening/bv_utils.cpp
+++ b/src/solvers/flattening/bv_utils.cpp
@@ -615,10 +615,10 @@ literalt bv_utilst::overflow_negate(const bvt &bv)
   // a overflow on unary- can only happen with the smallest
   // representable number 100....0
 
-  bvt zeros(bv);
-  zeros.erase(--zeros.end());
+  bvt should_be_zeros(bv);
+  should_be_zeros.pop_back();
 
-  return prop.land(bv[bv.size()-1], !prop.lor(zeros));
+  return prop.land(bv[bv.size() - 1], !prop.lor(should_be_zeros));
 }
 
 void bv_utilst::incrementer(

From 047c065efd9685c59f789dd9e9e293d9c6e70786 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 12 Sep 2022 05:44:31 +0000
Subject: [PATCH 3/3] bv_utilst::zeros: use the most appropriate constructor

There is no need to first create an empty bit vector and then populate
it. Use RAII instead.
---
 src/solvers/flattening/bv_utils.h | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/solvers/flattening/bv_utils.h b/src/solvers/flattening/bv_utils.h
index 1b988cda0c6..a282f446e32 100644
--- a/src/solvers/flattening/bv_utils.h
+++ b/src/solvers/flattening/bv_utils.h
@@ -191,9 +191,7 @@ class bv_utilst
 
   static bvt zeros(std::size_t new_size)
   {
-    bvt result;
-    result.resize(new_size, const_literal(false));
-    return result;
+    return bvt(new_size, const_literal(false));
   }
 
   void set_equal(const bvt &a, const bvt &b);