From ed2cf6a046b0e789b43c145fe49b5928c855c59a Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 22 Jun 2018 13:18:46 +0100
Subject: [PATCH] Remove unused parameter from float_bvt::is_zero

---
 src/solvers/floatbv/float_bv.cpp | 16 +++++++---------
 src/solvers/floatbv/float_bv.h   |  2 +-
 2 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/src/solvers/floatbv/float_bv.cpp b/src/solvers/floatbv/float_bv.cpp
index 162cd482720..28b322b7893 100644
--- a/src/solvers/floatbv/float_bv.cpp
+++ b/src/solvers/floatbv/float_bv.cpp
@@ -64,7 +64,7 @@ exprt float_bvt::convert(const exprt &expr)
   else if(expr.id()==ID_typecast &&
           expr.type().id()==ID_bool &&
           expr.op0().type().id()==ID_floatbv)  // float -> bool
-    return not_exprt(is_zero(expr.op0(), get_spec(expr.op0())));
+    return not_exprt(is_zero(expr.op0()));
   else if(expr.id()==ID_floatbv_plus)
     return add_sub(false, expr.op0(), expr.op1(), expr.op2(), get_spec(expr));
   else if(expr.id()==ID_floatbv_minus)
@@ -129,8 +129,8 @@ exprt float_bvt::is_equal(
   const ieee_float_spect &spec)
 {
   // special cases: -0 and 0 are equal
-  exprt is_zero0=is_zero(src0, spec);
-  exprt is_zero1=is_zero(src1, spec);
+  const exprt is_zero0 = is_zero(src0);
+  const exprt is_zero1 = is_zero(src1);
   const and_exprt both_zero(is_zero0, is_zero1);
 
   // NaN compares to nothing
@@ -145,9 +145,7 @@ exprt float_bvt::is_equal(
     not_exprt(nan));
 }
 
-exprt float_bvt::is_zero(
-  const exprt &src,
-  const ieee_float_spect &spec)
+exprt float_bvt::is_zero(const exprt &src)
 {
   // we mask away the sign bit, which is the most significant bit
   const floatbv_typet &type=to_floatbv_type(src.type());
@@ -743,8 +741,8 @@ exprt float_bvt::relation(
   assert(rel==relt::EQ || rel==relt::LT || rel==relt::LE);
 
   // special cases: -0 and 0 are equal
-  exprt is_zero1=is_zero(src1, spec);
-  exprt is_zero2=is_zero(src2, spec);
+  const exprt is_zero1 = is_zero(src1);
+  const exprt is_zero2 = is_zero(src2);
   const and_exprt both_zero(is_zero1, is_zero2);
 
   // NaN compares to nothing
@@ -1346,7 +1344,7 @@ float_bvt::unbiased_floatt float_bvt::unpack(
       sub_bias(result.exponent, spec));
 
   result.infinity=isinf(src, spec);
-  result.zero=is_zero(src, spec);
+  result.zero = is_zero(src);
   result.NaN=isnan(src, spec);
 
   return result;
diff --git a/src/solvers/floatbv/float_bv.h b/src/solvers/floatbv/float_bv.h
index 9c071b73e33..0beb935013b 100644
--- a/src/solvers/floatbv/float_bv.h
+++ b/src/solvers/floatbv/float_bv.h
@@ -36,7 +36,7 @@ class float_bvt
   exprt negation(const exprt &, const ieee_float_spect &);
   exprt abs(const exprt &, const ieee_float_spect &);
   exprt is_equal(const exprt &, const exprt &, const ieee_float_spect &);
-  exprt is_zero(const exprt &, const ieee_float_spect &);
+  exprt is_zero(const exprt &);
   exprt isnan(const exprt &, const ieee_float_spect &);
   exprt isinf(const exprt &, const ieee_float_spect &);
   exprt isnormal(const exprt &, const ieee_float_spect &);