From 35b24c61bd3123bd3306e59756d08b73a10b29c4 Mon Sep 17 00:00:00 2001
From: Daniel Poetzl <daniel.poetzl@diffblue.com>
Date: Wed, 12 Sep 2018 14:14:38 +0100
Subject: [PATCH 1/4] Add wellformedness checks to bitvector types in std_types

---
 src/util/std_types.h | 93 +++++++++++++++++++++++++++++++++++---------
 1 file changed, 75 insertions(+), 18 deletions(-)

diff --git a/src/util/std_types.h b/src/util/std_types.h
index c4b18bbbc6f..99c4d5abed1 100644
--- a/src/util/std_types.h
+++ b/src/util/std_types.h
@@ -1210,6 +1210,11 @@ inline bool can_cast_type<bv_typet>(const typet &type)
   return type.id() == ID_bv;
 }
 
+inline void validate_type(const bv_typet &type)
+{
+  DATA_INVARIANT(!type.get(ID_width).empty(), "bitvector type must have width");
+}
+
 /// \brief Cast a typet to a \ref bv_typet
 ///
 /// This is an unchecked conversion. \a type must be known to be \ref
@@ -1221,14 +1226,18 @@ inline bool can_cast_type<bv_typet>(const typet &type)
 inline const bv_typet &to_bv_type(const typet &type)
 {
   PRECONDITION(can_cast_type<bv_typet>(type));
-  return static_cast<const bv_typet &>(type);
+  const bv_typet &ret = static_cast<const bv_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /// \copydoc to_bv_type(const typet &)
 inline bv_typet &to_bv_type(typet &type)
 {
   PRECONDITION(can_cast_type<bv_typet>(type));
-  return static_cast<bv_typet &>(type);
+  bv_typet &ret = static_cast<bv_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /// Fixed-width bit-vector with unsigned binary interpretation
@@ -1256,6 +1265,12 @@ inline bool can_cast_type<unsignedbv_typet>(const typet &type)
   return type.id() == ID_unsignedbv;
 }
 
+inline void validate_type(const unsignedbv_typet &type)
+{
+  DATA_INVARIANT(
+    !type.get(ID_width).empty(), "unsigned bitvector type must have width");
+}
+
 /// \brief Cast a typet to an \ref unsignedbv_typet
 ///
 /// This is an unchecked conversion. \a type must be known to be \ref
@@ -1267,14 +1282,18 @@ inline bool can_cast_type<unsignedbv_typet>(const typet &type)
 inline const unsignedbv_typet &to_unsignedbv_type(const typet &type)
 {
   PRECONDITION(can_cast_type<unsignedbv_typet>(type));
-  return static_cast<const unsignedbv_typet &>(type);
+  const unsignedbv_typet &ret = static_cast<const unsignedbv_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /// \copydoc to_unsignedbv_type(const typet &)
 inline unsignedbv_typet &to_unsignedbv_type(typet &type)
 {
   PRECONDITION(can_cast_type<unsignedbv_typet>(type));
-  return static_cast<unsignedbv_typet &>(type);
+  unsignedbv_typet &ret = static_cast<unsignedbv_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /// Fixed-width bit-vector with two's complement interpretation
@@ -1302,6 +1321,12 @@ inline bool can_cast_type<signedbv_typet>(const typet &type)
   return type.id() == ID_signedbv;
 }
 
+inline void validate_type(const signedbv_typet &type)
+{
+  DATA_INVARIANT(
+    !type.get(ID_width).empty(), "signed bitvector type must have width");
+}
+
 /// \brief Cast a typet to a \ref signedbv_typet
 ///
 /// This is an unchecked conversion. \a type must be known to be \ref
@@ -1313,14 +1338,18 @@ inline bool can_cast_type<signedbv_typet>(const typet &type)
 inline const signedbv_typet &to_signedbv_type(const typet &type)
 {
   PRECONDITION(can_cast_type<signedbv_typet>(type));
-  return static_cast<const signedbv_typet &>(type);
+  const signedbv_typet &ret = static_cast<const signedbv_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /// \copydoc to_signedbv_type(const typet &)
 inline signedbv_typet &to_signedbv_type(typet &type)
 {
   PRECONDITION(can_cast_type<signedbv_typet>(type));
-  return static_cast<signedbv_typet &>(type);
+  signedbv_typet &ret = static_cast<signedbv_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /// Fixed-width bit-vector with signed fixed-point interpretation
@@ -1356,6 +1385,12 @@ inline bool can_cast_type<fixedbv_typet>(const typet &type)
   return type.id() == ID_fixedbv;
 }
 
+inline void validate_type(const fixedbv_typet &type)
+{
+  DATA_INVARIANT(
+    !type.get(ID_width).empty(), "fixed bitvector type must have width");
+}
+
 /// \brief Cast a typet to a \ref fixedbv_typet
 ///
 /// This is an unchecked conversion. \a type must be known to be \ref
@@ -1367,14 +1402,18 @@ inline bool can_cast_type<fixedbv_typet>(const typet &type)
 inline const fixedbv_typet &to_fixedbv_type(const typet &type)
 {
   PRECONDITION(can_cast_type<fixedbv_typet>(type));
-  return static_cast<const fixedbv_typet &>(type);
+  const fixedbv_typet &ret = static_cast<const fixedbv_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /// \copydoc to_fixedbv_type(const typet &)
 inline fixedbv_typet &to_fixedbv_type(typet &type)
 {
   PRECONDITION(can_cast_type<fixedbv_typet>(type));
-  return static_cast<fixedbv_typet &>(type);
+  fixedbv_typet &ret = static_cast<fixedbv_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /// Fixed-width bit-vector with IEEE floating-point interpretation
@@ -1408,6 +1447,12 @@ inline bool can_cast_type<floatbv_typet>(const typet &type)
   return type.id() == ID_floatbv;
 }
 
+inline void validate_type(const floatbv_typet &type)
+{
+  DATA_INVARIANT(
+    !type.get(ID_width).empty(), "float bitvector type must have width");
+}
+
 /// \brief Cast a typet to a \ref floatbv_typet
 ///
 /// This is an unchecked conversion. \a type must be known to be \ref
@@ -1419,14 +1464,18 @@ inline bool can_cast_type<floatbv_typet>(const typet &type)
 inline const floatbv_typet &to_floatbv_type(const typet &type)
 {
   PRECONDITION(can_cast_type<floatbv_typet>(type));
-  return static_cast<const floatbv_typet &>(type);
+  const floatbv_typet &ret = static_cast<const floatbv_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /// \copydoc to_floatbv_type(const typet &)
 inline floatbv_typet &to_floatbv_type(typet &type)
 {
   PRECONDITION(can_cast_type<floatbv_typet>(type));
-  return static_cast<floatbv_typet &>(type);
+  floatbv_typet &ret = static_cast<floatbv_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /// Type for C bit fields
@@ -1495,6 +1544,11 @@ inline bool can_cast_type<pointer_typet>(const typet &type)
   return type.id() == ID_pointer;
 }
 
+inline void validate_type(const pointer_typet &type)
+{
+  DATA_INVARIANT(!type.get(ID_width).empty(), "pointer must have width");
+}
+
 /// \brief Cast a typet to a \ref pointer_typet
 ///
 /// This is an unchecked conversion. \a type must be known to be \ref
@@ -1520,12 +1574,6 @@ inline pointer_typet &to_pointer_type(typet &type)
   return ret;
 }
 
-inline void validate_type(const pointer_typet &type)
-{
-  DATA_INVARIANT(!type.get(ID_width).empty(), "pointer must have width");
-  DATA_INVARIANT(type.get_width() > 0, "pointer must have non-zero width");
-}
-
 /// The reference type
 ///
 /// Intends to model C++ reference. Comparing to \ref pointer_typet should
@@ -1598,6 +1646,11 @@ inline bool can_cast_type<c_bool_typet>(const typet &type)
   return type.id() == ID_c_bool;
 }
 
+inline void validate_type(const c_bool_typet &type)
+{
+  DATA_INVARIANT(!type.get(ID_width).empty(), "C bool type must have width");
+}
+
 /// \brief Cast a typet to a \ref c_bool_typet
 ///
 /// This is an unchecked conversion. \a type must be known to be \ref
@@ -1609,14 +1662,18 @@ inline bool can_cast_type<c_bool_typet>(const typet &type)
 inline const c_bool_typet &to_c_bool_type(const typet &type)
 {
   PRECONDITION(can_cast_type<c_bool_typet>(type));
-  return static_cast<const c_bool_typet &>(type);
+  const c_bool_typet &ret = static_cast<const c_bool_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /// \copydoc to_c_bool_type(const typet &)
 inline c_bool_typet &to_c_bool_type(typet &type)
 {
   PRECONDITION(can_cast_type<c_bool_typet>(type));
-  return static_cast<c_bool_typet &>(type);
+  c_bool_typet &ret = static_cast<c_bool_typet &>(type);
+  validate_type(ret);
+  return ret;
 }
 
 /// String type

From db9688e758e0462af5f6fdaeb0e2f44e67859d68 Mon Sep 17 00:00:00 2001
From: Daniel Poetzl <daniel.poetzl@diffblue.com>
Date: Mon, 24 Sep 2018 12:33:50 +0100
Subject: [PATCH 2/4] Error handling cleanup in solvers/flattening

Files boolbv_unary_minus.cpp to boolbv_with.cpp
---
 src/solvers/flattening/boolbv.cpp             |  2 +-
 src/solvers/flattening/boolbv.h               |  2 +-
 src/solvers/flattening/boolbv_unary_minus.cpp | 37 ++++++++++---------
 src/solvers/flattening/boolbv_union.cpp       | 11 ++++--
 src/solvers/flattening/boolbv_vector.cpp      | 34 +++++++----------
 src/solvers/flattening/boolbv_width.cpp       | 23 +++++-------
 6 files changed, 51 insertions(+), 58 deletions(-)

diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
index 53f1cdcb44e..b568c0d2c3b 100644
--- a/src/solvers/flattening/boolbv.cpp
+++ b/src/solvers/flattening/boolbv.cpp
@@ -281,7 +281,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   else if(expr.id()==ID_array)
     return convert_array(expr);
   else if(expr.id()==ID_vector)
-    return convert_vector(expr);
+    return convert_vector(to_vector_expr(expr));
   else if(expr.id()==ID_complex)
     return convert_complex(to_complex_expr(expr));
   else if(expr.id()==ID_complex_real)
diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h
index c51f3a3803b..85e3cccf540 100644
--- a/src/solvers/flattening/boolbv.h
+++ b/src/solvers/flattening/boolbv.h
@@ -142,7 +142,7 @@ class boolbvt:public arrayst
   virtual bvt convert_if(const if_exprt &expr);
   virtual bvt convert_struct(const struct_exprt &expr);
   virtual bvt convert_array(const exprt &expr);
-  virtual bvt convert_vector(const exprt &expr);
+  virtual bvt convert_vector(const vector_exprt &expr);
   virtual bvt convert_complex(const complex_exprt &expr);
   virtual bvt convert_complex_real(const complex_real_exprt &expr);
   virtual bvt convert_complex_imag(const complex_imag_exprt &expr);
diff --git a/src/solvers/flattening/boolbv_unary_minus.cpp b/src/solvers/flattening/boolbv_unary_minus.cpp
index 05424f29914..03efceac5ce 100644
--- a/src/solvers/flattening/boolbv_unary_minus.cpp
+++ b/src/solvers/flattening/boolbv_unary_minus.cpp
@@ -23,24 +23,15 @@ bvt boolbvt::convert_unary_minus(const unary_exprt &expr)
   if(width==0)
     return conversion_failed(expr);
 
-  const exprt::operandst &operands=expr.operands();
+  const exprt &op = expr.op();
 
-  if(operands.size()!=1)
-    throw "unary minus takes one operand";
-
-  const exprt &op0=expr.op0();
-
-  const bvt &op_bv=convert_bv(op0);
+  const bvt &op_bv = convert_bv(op, width);
 
   bvtypet bvtype=get_bvtype(type);
-  bvtypet op_bvtype=get_bvtype(op0.type());
-  std::size_t op_width=op_bv.size();
+  bvtypet op_bvtype = get_bvtype(op.type());
 
   bool no_overflow=(expr.id()=="no-overflow-unary-minus");
 
-  if(op_width==0 || op_width!=width)
-    return conversion_failed(expr);
-
   if(bvtype==bvtypet::IS_UNKNOWN &&
      (type.id()==ID_vector || type.id()==ID_complex))
   {
@@ -48,8 +39,14 @@ bvt boolbvt::convert_unary_minus(const unary_exprt &expr)
 
     std::size_t sub_width=boolbv_width(subtype);
 
-    if(sub_width==0 || width%sub_width!=0)
-      throw "unary-: unexpected vector operand width";
+    INVARIANT(
+      sub_width > 0,
+      "bitvector representation of type needs to have at least one bit");
+
+    INVARIANT(
+      width % sub_width == 0,
+      "total bitvector width needs to be a multiple of the component bitvector "
+      "widths");
 
     std::size_t size=width/sub_width;
     bvt bv;
@@ -62,7 +59,8 @@ bvt boolbvt::convert_unary_minus(const unary_exprt &expr)
 
       for(std::size_t j=0; j<tmp_op.size(); j++)
       {
-        assert(i*sub_width+j<op_bv.size());
+        INVARIANT(
+          i * sub_width + j < op_bv.size(), "bit index shall be within bounds");
         tmp_op[j]=op_bv[i*sub_width+j];
       }
 
@@ -76,11 +74,14 @@ bvt boolbvt::convert_unary_minus(const unary_exprt &expr)
       else
         tmp_result=bv_utils.negate(tmp_op);
 
-      assert(tmp_result.size()==sub_width);
+      INVARIANT(
+        tmp_result.size() == sub_width,
+        "bitvector after negation shall have same bit width");
 
       for(std::size_t j=0; j<tmp_result.size(); j++)
       {
-        assert(i*sub_width+j<bv.size());
+        INVARIANT(
+          i * sub_width + j < bv.size(), "bit index shall be within bounds");
         bv[i*sub_width+j]=tmp_result[j];
       }
     }
@@ -96,7 +97,7 @@ bvt boolbvt::convert_unary_minus(const unary_exprt &expr)
   }
   else if(bvtype==bvtypet::IS_FLOAT && op_bvtype==bvtypet::IS_FLOAT)
   {
-    assert(!no_overflow);
+    INVARIANT(!no_overflow, "");
     float_utilst float_utils(prop, to_floatbv_type(expr.type()));
     return float_utils.negate(op_bv);
   }
diff --git a/src/solvers/flattening/boolbv_union.cpp b/src/solvers/flattening/boolbv_union.cpp
index cd9a290882d..fb196135893 100644
--- a/src/solvers/flattening/boolbv_union.cpp
+++ b/src/solvers/flattening/boolbv_union.cpp
@@ -22,8 +22,10 @@ bvt boolbvt::convert_union(const union_exprt &expr)
 
   const bvt &op_bv=convert_bv(expr.op());
 
-  if(width<op_bv.size())
-    throw "union: unexpected operand op width";
+  INVARIANT(
+    op_bv.size() <= width,
+    "operand bitvector width shall not be larger than the width indicated by "
+    "the union type");
 
   bvt bv;
   bv.resize(width);
@@ -39,8 +41,9 @@ bvt boolbvt::convert_union(const union_exprt &expr)
   }
   else
   {
-    assert(
-      config.ansi_c.endianness==configt::ansi_ct::endiannesst::IS_BIG_ENDIAN);
+    INVARIANT(
+      config.ansi_c.endianness == configt::ansi_ct::endiannesst::IS_BIG_ENDIAN,
+      "endianness should be set to either little endian or big endian");
 
     bv_endianness_mapt map_u(expr.type(), false, ns, boolbv_width);
     bv_endianness_mapt map_op(expr.op0().type(), false, ns, boolbv_width);
diff --git a/src/solvers/flattening/boolbv_vector.cpp b/src/solvers/flattening/boolbv_vector.cpp
index 07b5397111d..a0f55fadb3b 100644
--- a/src/solvers/flattening/boolbv_vector.cpp
+++ b/src/solvers/flattening/boolbv_vector.cpp
@@ -9,38 +9,30 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "boolbv.h"
 
-bvt boolbvt::convert_vector(const exprt &expr)
+bvt boolbvt::convert_vector(const vector_exprt &expr)
 {
   std::size_t width=boolbv_width(expr.type());
 
   if(width==0)
     return conversion_failed(expr);
 
-  if(expr.type().id()==ID_vector)
-  {
-    const exprt::operandst &operands=expr.operands();
-
-    bvt bv;
-    bv.reserve(width);
+  const exprt::operandst &operands = expr.operands();
 
-    if(!operands.empty())
-    {
-      std::size_t op_width=width/operands.size();
+  bvt bv;
+  bv.reserve(width);
 
-      forall_expr(it, operands)
-      {
-        const bvt &tmp=convert_bv(*it);
+  if(!operands.empty())
+  {
+    std::size_t op_width = width / operands.size();
 
-        if(tmp.size()!=op_width)
-          throw "convert_vector: unexpected operand width";
+    forall_expr(it, operands)
+    {
+      const bvt &tmp = convert_bv(*it, op_width);
 
-        forall_literals(it2, tmp)
-          bv.push_back(*it2);
-      }
+      forall_literals(it2, tmp)
+        bv.push_back(*it2);
     }
-
-    return bv;
   }
 
-  return conversion_failed(expr);
+  return bv;
 }
diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp
index 16dfabf59a6..df8bac8821d 100644
--- a/src/solvers/flattening/boolbv_width.cpp
+++ b/src/solvers/flattening/boolbv_width.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <algorithm>
 
 #include <util/arith_tools.h>
+#include <util/exception_utils.h>
 #include <util/invariant.h>
 #include <util/std_types.h>
 
@@ -79,39 +80,35 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
   else if(type_id==ID_c_bool)
   {
     entry.total_width=to_c_bool_type(type).get_width();
-    assert(entry.total_width!=0);
   }
   else if(type_id==ID_signedbv)
   {
     entry.total_width=to_signedbv_type(type).get_width();
-    assert(entry.total_width!=0);
   }
   else if(type_id==ID_unsignedbv)
   {
     entry.total_width=to_unsignedbv_type(type).get_width();
-    assert(entry.total_width!=0);
   }
   else if(type_id==ID_floatbv)
   {
     entry.total_width=to_floatbv_type(type).get_width();
-    assert(entry.total_width!=0);
   }
   else if(type_id==ID_fixedbv)
   {
     entry.total_width=to_fixedbv_type(type).get_width();
-    assert(entry.total_width!=0);
   }
   else if(type_id==ID_bv)
   {
     entry.total_width=to_bv_type(type).get_width();
-    assert(entry.total_width!=0);
   }
   else if(type_id==ID_verilog_signedbv ||
           type_id==ID_verilog_unsignedbv)
   {
     // we encode with two bits
-    entry.total_width = type.get_size_t(ID_width) * 2;
-    assert(entry.total_width!=0);
+    std::size_t size = type.get_size_t(ID_width);
+    DATA_INVARIANT(
+      size > 0, "verilog bitvector width shall be greater than zero");
+    entry.total_width = size * 2;
   }
   else if(type_id==ID_range)
   {
@@ -123,7 +120,7 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
     if(size>=1)
     {
       entry.total_width = address_bits(size);
-      assert(entry.total_width!=0);
+      CHECK_RETURN(entry.total_width > 0);
     }
   }
   else if(type_id==ID_array)
@@ -142,7 +139,7 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
     {
       mp_integer total=array_size*sub_width;
       if(total>(1<<30)) // realistic limit
-        throw "array too large for flattening";
+        throw analysis_exceptiont("array too large for flattening");
 
       entry.total_width=integer2unsigned(total);
     }
@@ -163,7 +160,7 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
     {
       mp_integer total=vector_size*sub_width;
       if(total>(1<<30)) // realistic limit
-        throw "vector too large for flattening";
+        analysis_exceptiont("vector too large for flattening");
 
       entry.total_width=integer2unsigned(vector_size*sub_width);
     }
@@ -181,13 +178,13 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
     // get number of necessary bits
     std::size_t size=to_enumeration_type(type).elements().size();
     entry.total_width = address_bits(size);
-    assert(entry.total_width!=0);
+    CHECK_RETURN(entry.total_width > 0);
   }
   else if(type_id==ID_c_enum)
   {
     // these have a subtype
     entry.total_width = type.subtype().get_size_t(ID_width);
-    assert(entry.total_width!=0);
+    CHECK_RETURN(entry.total_width > 0);
   }
   else if(type_id==ID_incomplete_c_enum)
   {

From 0c17c04c243d6bff59b160f08a6163de43eaf879 Mon Sep 17 00:00:00 2001
From: Daniel Poetzl <daniel.poetzl@diffblue.com>
Date: Mon, 24 Sep 2018 12:50:13 +0100
Subject: [PATCH 3/4] Refactor iteration over bitvector in
 convert_unary_minus()

---
 src/solvers/flattening/boolbv_unary_minus.cpp | 33 +++++++------------
 1 file changed, 11 insertions(+), 22 deletions(-)

diff --git a/src/solvers/flattening/boolbv_unary_minus.cpp b/src/solvers/flattening/boolbv_unary_minus.cpp
index 03efceac5ce..03fbfd99af2 100644
--- a/src/solvers/flattening/boolbv_unary_minus.cpp
+++ b/src/solvers/flattening/boolbv_unary_minus.cpp
@@ -12,6 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <solvers/floatbv/float_utils.h>
 
+#include <algorithm>
+#include <iterator>
+
 #include "boolbv_type.h"
 
 bvt boolbvt::convert_unary_minus(const unary_exprt &expr)
@@ -48,42 +51,28 @@ bvt boolbvt::convert_unary_minus(const unary_exprt &expr)
       "total bitvector width needs to be a multiple of the component bitvector "
       "widths");
 
-    std::size_t size=width/sub_width;
     bvt bv;
-    bv.resize(width);
 
-    for(std::size_t i=0; i<size; i++)
+    for(std::size_t sub_idx = 0; sub_idx < width; sub_idx += sub_width)
     {
       bvt tmp_op;
-      tmp_op.resize(sub_width);
-
-      for(std::size_t j=0; j<tmp_op.size(); j++)
-      {
-        INVARIANT(
-          i * sub_width + j < op_bv.size(), "bit index shall be within bounds");
-        tmp_op[j]=op_bv[i*sub_width+j];
-      }
 
-      bvt tmp_result;
+      const auto sub_it = std::next(op_bv.begin(), sub_idx);
+      std::copy_n(sub_it, sub_width, std::back_inserter(tmp_op));
 
-      if(type.subtype().id()==ID_floatbv)
+      if(type.subtype().id() == ID_floatbv)
       {
         float_utilst float_utils(prop, to_floatbv_type(subtype));
-        tmp_result=float_utils.negate(tmp_op);
+        tmp_op = float_utils.negate(tmp_op);
       }
       else
-        tmp_result=bv_utils.negate(tmp_op);
+        tmp_op = bv_utils.negate(tmp_op);
 
       INVARIANT(
-        tmp_result.size() == sub_width,
+        tmp_op.size() == sub_width,
         "bitvector after negation shall have same bit width");
 
-      for(std::size_t j=0; j<tmp_result.size(); j++)
-      {
-        INVARIANT(
-          i * sub_width + j < bv.size(), "bit index shall be within bounds");
-        bv[i*sub_width+j]=tmp_result[j];
-      }
+      std::copy(tmp_op.begin(), tmp_op.end(), std::back_inserter(bv));
     }
 
     return bv;

From 7d629c5ae25910d1274f476b1327e84c43b73069 Mon Sep 17 00:00:00 2001
From: Daniel Poetzl <daniel.poetzl@diffblue.com>
Date: Sun, 23 Sep 2018 20:06:07 +0100
Subject: [PATCH 4/4] Remove "no-overflow-unary-minus" expressions

---
 src/solvers/flattening/boolbv.cpp             |  5 ++---
 src/solvers/flattening/boolbv.h               |  2 +-
 src/solvers/flattening/boolbv_unary_minus.cpp | 18 +++---------------
 3 files changed, 6 insertions(+), 19 deletions(-)

diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
index b568c0d2c3b..8eb8a1bea57 100644
--- a/src/solvers/flattening/boolbv.cpp
+++ b/src/solvers/flattening/boolbv.cpp
@@ -251,9 +251,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
           expr.id()==ID_bitxnor || expr.id()==ID_bitnor ||
           expr.id()==ID_bitnand)
     return convert_bitwise(expr);
-  else if(expr.id()==ID_unary_minus ||
-          expr.id()=="no-overflow-unary-minus")
-    return convert_unary_minus(to_unary_expr(expr));
+  else if(expr.id() == ID_unary_minus)
+    return convert_unary_minus(to_unary_minus_expr(expr));
   else if(expr.id()==ID_unary_plus)
   {
     return convert_bitvector(to_unary_plus_expr(expr).op());
diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h
index 85e3cccf540..94e1860a057 100644
--- a/src/solvers/flattening/boolbv.h
+++ b/src/solvers/flattening/boolbv.h
@@ -164,7 +164,7 @@ class boolbvt:public arrayst
   virtual bvt convert_cond(const exprt &expr);
   virtual bvt convert_shift(const binary_exprt &expr);
   virtual bvt convert_bitwise(const exprt &expr);
-  virtual bvt convert_unary_minus(const unary_exprt &expr);
+  virtual bvt convert_unary_minus(const unary_minus_exprt &expr);
   virtual bvt convert_abs(const abs_exprt &expr);
   virtual bvt convert_concatenation(const concatenation_exprt &expr);
   virtual bvt convert_replication(const replication_exprt &expr);
diff --git a/src/solvers/flattening/boolbv_unary_minus.cpp b/src/solvers/flattening/boolbv_unary_minus.cpp
index 03fbfd99af2..77d8498bb76 100644
--- a/src/solvers/flattening/boolbv_unary_minus.cpp
+++ b/src/solvers/flattening/boolbv_unary_minus.cpp
@@ -17,7 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "boolbv_type.h"
 
-bvt boolbvt::convert_unary_minus(const unary_exprt &expr)
+bvt boolbvt::convert_unary_minus(const unary_minus_exprt &expr)
 {
   const typet &type=ns.follow(expr.type());
 
@@ -33,8 +33,6 @@ bvt boolbvt::convert_unary_minus(const unary_exprt &expr)
   bvtypet bvtype=get_bvtype(type);
   bvtypet op_bvtype = get_bvtype(op.type());
 
-  bool no_overflow=(expr.id()=="no-overflow-unary-minus");
-
   if(bvtype==bvtypet::IS_UNKNOWN &&
      (type.id()==ID_vector || type.id()==ID_complex))
   {
@@ -79,27 +77,17 @@ bvt boolbvt::convert_unary_minus(const unary_exprt &expr)
   }
   else if(bvtype==bvtypet::IS_FIXED && op_bvtype==bvtypet::IS_FIXED)
   {
-    if(no_overflow)
-      return bv_utils.negate_no_overflow(op_bv);
-    else
-      return bv_utils.negate(op_bv);
+    return bv_utils.negate(op_bv);
   }
   else if(bvtype==bvtypet::IS_FLOAT && op_bvtype==bvtypet::IS_FLOAT)
   {
-    INVARIANT(!no_overflow, "");
     float_utilst float_utils(prop, to_floatbv_type(expr.type()));
     return float_utils.negate(op_bv);
   }
   else if((op_bvtype==bvtypet::IS_SIGNED || op_bvtype==bvtypet::IS_UNSIGNED) &&
           (bvtype==bvtypet::IS_SIGNED || bvtype==bvtypet::IS_UNSIGNED))
   {
-    if(no_overflow)
-      prop.l_set_to(bv_utils.overflow_negate(op_bv), false);
-
-    if(no_overflow)
-      return bv_utils.negate_no_overflow(op_bv);
-    else
-      return bv_utils.negate(op_bv);
+    return bv_utils.negate(op_bv);
   }
 
   return conversion_failed(expr);