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));
// 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);
}
}