From 0e2b13f41d39314b3f61a4109cc9f3bf11a34fa5 Mon Sep 17 00:00:00 2001
From: reuk <reuk@users.noreply.github.com>
Date: Mon, 2 Oct 2017 14:58:07 +0100
Subject: [PATCH 1/3] Remove tautological typecasts

---
 src/util/simplify_expr.cpp | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 5d0e00b4b2e..d601ef06e3f 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -240,6 +240,18 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
   if(expr_type.id()==ID_c_bool &&
      op_type.id()!=ID_bool)
   {
+    // casts from boolean to a signed int and back:
+    // (boolean)(int)boolean -> boolean
+    if(expr.op0().id()==ID_typecast && op_type.id()==ID_signedbv)
+    {
+      const auto &typecast=to_typecast_expr(expr.op0());
+      if(typecast.op().type().id()==ID_c_bool)
+      {
+        expr=typecast.op0();
+        return false;
+      }
+    }
+
     // rewrite (_Bool)x to (_Bool)(x!=0)
     binary_relation_exprt inequality;
     inequality.id(op_type.id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal);

From 9ea7414f5f37e07fc05ccbe8a19592582dbbdc3f Mon Sep 17 00:00:00 2001
From: reuk <reuk@users.noreply.github.com>
Date: Tue, 3 Oct 2017 13:44:01 +0100
Subject: [PATCH 2/3] Set up config in unit tests

---
 unit/util/simplify_expr.cpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp
index 20d5816a8e9..9b87101984f 100644
--- a/unit/util/simplify_expr.cpp
+++ b/unit/util/simplify_expr.cpp
@@ -10,6 +10,7 @@
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/namespace.h>
 #include <util/pointer_predicates.h>
 #include <util/simplify_expr.h>
@@ -18,6 +19,8 @@
 
 TEST_CASE("Simplify pointer_offset(address of array index)")
 {
+  config.set_arch("none");
+
   symbol_tablet symbol_table;
   namespacet ns(symbol_table);
 
@@ -38,6 +41,8 @@ TEST_CASE("Simplify pointer_offset(address of array index)")
 
 TEST_CASE("Simplify const pointer offset")
 {
+  config.set_arch("none");
+
   symbol_tablet symbol_table;
   namespacet ns(symbol_table);
 

From 1d879289f8e987022b98b125cfe531a586b09a3b Mon Sep 17 00:00:00 2001
From: reuk <reuk@users.noreply.github.com>
Date: Tue, 3 Oct 2017 14:00:15 +0100
Subject: [PATCH 3/3] Add unit test for new behavior

---
 unit/util/simplify_expr.cpp | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp
index 9b87101984f..053fa11d7e3 100644
--- a/unit/util/simplify_expr.cpp
+++ b/unit/util/simplify_expr.cpp
@@ -8,6 +8,7 @@
 
 #include <catch.hpp>
 
+#include <java_bytecode/java_types.h>
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
@@ -59,3 +60,23 @@ TEST_CASE("Simplify const pointer offset")
   REQUIRE(!to_integer(simp, offset_value));
   REQUIRE(offset_value==1234);
 }
+
+TEST_CASE("Simplify Java boolean -> int -> boolean casts")
+{
+  config.set_arch("none");
+
+  const exprt simplified=simplify_expr(
+    typecast_exprt(
+      typecast_exprt(
+        symbol_exprt(
+          "foo",
+          java_boolean_type()),
+        java_int_type()),
+      java_boolean_type()),
+    namespacet(symbol_tablet()));
+
+  REQUIRE(simplified.id()==ID_symbol);
+  REQUIRE(simplified.type()==java_boolean_type());
+  const auto &symbol=to_symbol_expr(simplified);
+  REQUIRE(symbol.get_identifier()=="foo");
+}