From 60906b16bfb70c8aaef129dfd8eee88e2668a8d2 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Wed, 9 Aug 2017 19:37:21 +0200
Subject: [PATCH] simplifier: erase 'all ones' out of bitand

---
 src/util/simplify_expr_int.cpp | 24 +++++++++++++++++++++++-
 1 file changed, 23 insertions(+), 1 deletion(-)

diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index d103ea79bb7..a94674c3fd9 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -664,7 +664,7 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
     result=false;
   }
 
-  // now erase zeros out of bitor, bitxor
+  // now erase 'all zeros' out of bitor, bitxor
 
   if(expr.id()==ID_bitor || expr.id()==ID_bitxor)
   {
@@ -683,6 +683,28 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
     }
   }
 
+  // now erase 'all ones' out of bitand
+
+  if(expr.id()==ID_bitand)
+  {
+    for(exprt::operandst::iterator
+        it=expr.operands().begin();
+        it!=expr.operands().end();
+        ) // no it++
+    {
+      if(it->is_constant() &&
+         id2string(to_constant_expr(*it).get_value()).find('0')==
+           std::string::npos &&
+         expr.operands().size()>1)
+      {
+        it=expr.operands().erase(it);
+        result=false;
+      }
+      else
+        it++;
+    }
+  }
+
   // two operands that are syntactically the same
 
   if(expr.operands().size()==2 &&