From 9986ea139e6b0f285ecda5d250a6c87046bf0ded Mon Sep 17 00:00:00 2001
From: Chris Ryder <chris.ryder@diffblue.com>
Date: Mon, 23 Jul 2018 11:53:35 +0100
Subject: [PATCH 1/2] Make exprt::is_zero() support bitfields

---
 src/util/expr.cpp  |  3 ++-
 unit/Makefile      |  1 +
 unit/util/expr.cpp | 39 +++++++++++++++++++++++++++++++++++++++
 3 files changed, 42 insertions(+), 1 deletion(-)
 create mode 100644 unit/util/expr.cpp

diff --git a/src/util/expr.cpp b/src/util/expr.cpp
index af2cff9946f..8104e65e4de 100644
--- a/src/util/expr.cpp
+++ b/src/util/expr.cpp
@@ -178,7 +178,8 @@ bool exprt::is_zero() const
     }
     else if(type_id==ID_unsignedbv ||
             type_id==ID_signedbv ||
-            type_id==ID_c_bool)
+            type_id==ID_c_bool ||
+            type_id==ID_c_bit_field)
     {
       return constant.value_is_zero_string();
     }
diff --git a/unit/Makefile b/unit/Makefile
index 1f92f2be2d6..f0a5bb294cd 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -24,6 +24,7 @@ SRC += unit_tests.cpp \
        solvers/refinement/string_refinement/substitute_array_list.cpp \
        solvers/refinement/string_refinement/sparse_array.cpp \
        solvers/refinement/string_refinement/union_find_replace.cpp \
+       util/expr.cpp \
        util/expr_cast/expr_cast.cpp \
        util/graph.cpp \
        util/irep.cpp \
diff --git a/unit/util/expr.cpp b/unit/util/expr.cpp
new file mode 100644
index 00000000000..2f6d172fa70
--- /dev/null
+++ b/unit/util/expr.cpp
@@ -0,0 +1,39 @@
+/*******************************************************************\
+
+Module: Unit test for expr.h/expr.cpp
+
+Author: Diffblue Ltd
+
+\*******************************************************************/
+
+#include <testing-utils/catch.hpp>
+
+#include <util/arith_tools.h>
+#include <util/expr.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
+
+
+SCENARIO("bitfield-expr-is-zero", "[core][util][expr]")
+{
+  GIVEN("An exprt representing a bitfield constant of 3")
+  {
+    const exprt bitfield3 =
+      from_integer(mp_integer(3), c_bit_field_typet(signedbv_typet(32), 4));
+
+    THEN("is_zero() should be false")
+    {
+      REQUIRE_FALSE(bitfield3.is_zero());
+    }
+  }
+  GIVEN("An exprt representing a bitfield constant of 0")
+  {
+    const exprt bitfield0 =
+      from_integer(mp_integer(0), c_bit_field_typet(signedbv_typet(32), 4));
+
+    THEN("is_zero() should be true")
+    {
+      REQUIRE(bitfield0.is_zero());
+    }
+  }
+}

From 54cc8187f6bd96b9faea8a707fb60c694f5e269a Mon Sep 17 00:00:00 2001
From: Chris Ryder <chris.ryder@diffblue.com>
Date: Wed, 25 Jul 2018 17:15:55 +0100
Subject: [PATCH 2/2] clang-format fixups

---
 src/util/expr.cpp | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/util/expr.cpp b/src/util/expr.cpp
index 8104e65e4de..9c672b1051e 100644
--- a/src/util/expr.cpp
+++ b/src/util/expr.cpp
@@ -176,10 +176,9 @@ bool exprt::is_zero() const
         CHECK_RETURN(false);
       return rat_value.is_zero();
     }
-    else if(type_id==ID_unsignedbv ||
-            type_id==ID_signedbv ||
-            type_id==ID_c_bool ||
-            type_id==ID_c_bit_field)
+    else if(
+      type_id == ID_unsignedbv || type_id == ID_signedbv ||
+      type_id == ID_c_bool || type_id == ID_c_bit_field)
     {
       return constant.value_is_zero_string();
     }