From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 25 Jan 2022 03:22:48 +0000 (-0800)
Subject: [FP] Fix unused variable warning (#7977)
X-Git-Tag: cvc5-1.0.0~511
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=44232973fcb5b09d5440ef25cdb969fe4ad37962;p=cvc5.git

[FP] Fix unused variable warning (#7977)
---

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index bcbd9e297..547e52503 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -855,10 +855,16 @@ bool TheoryFp::collectModelValues(TheoryModel* m,
           nm->mkNode(kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND, node);
 
       eq::EqualityEngine* ee = m->getEqualityEngine();
-      Assert(ee->hasTerm(compNaN) && ee->getRepresentative(compNaN).isConst());
-      Assert(ee->hasTerm(compInf) && ee->getRepresentative(compInf).isConst());
-      Assert(ee->hasTerm(compZero)
-             && ee->getRepresentative(compZero).isConst());
+      Assert(ee->hasTerm(compNaN));
+      Assert(ee->hasTerm(compInf));
+      Assert(ee->hasTerm(compZero));
+      TNode rCompNaN = ee->getRepresentative(compNaN);
+      TNode rCompInf = ee->getRepresentative(compInf);
+      TNode rCompZero = ee->getRepresentative(compZero);
+      Assert(rCompNaN.isConst());
+      Assert(rCompInf.isConst());
+      Assert(rCompZero.isConst());
+
       Assert(ee->hasTerm(compExponent)
              && ee->getRepresentative(compExponent).isConst());
       Assert(ee->hasTerm(compSignificand));
@@ -866,11 +872,9 @@ bool TheoryFp::collectModelValues(TheoryModel* m,
 
       // At most one of the flags (NaN, inf, zero) can be set
       Node one = nm->mkConst(BitVector(1U, 1U));
-      size_t numFlags = 0;
-      numFlags += ee->getRepresentative(compNaN) == one ? 1 : 0;
-      numFlags += ee->getRepresentative(compInf) == one ? 1 : 0;
-      numFlags += ee->getRepresentative(compZero) == one ? 1 : 0;
-      Assert(numFlags <= 1);
+      Assert((rCompNaN == one ? 1 : 0) + (rCompInf == one ? 1 : 0)
+                 + (rCompZero == one ? 1 : 0)
+             <= 1);
     }
   }