Bug: same conditions found. It is very likely a copy-paste bug.

[ustchcs-bugfinder]

z3/src/util/mpf.cpp

Line 748 in 558233d

SASSERT(x.sbits == y.sbits && x.ebits == y.ebits &&

z3/src/util/mpf.cpp

Line 749 in 558233d

x.sbits == y.sbits && z.ebits == z.ebits);

x.sbits == y.sbits appears twice.

z.ebits == z.ebits is always true.

It is very likely a copy-paste bug.

SASSERT(x.sbits == y.sbits && x.ebits == y.ebits &&
               x.sbits == y.sbits && z.ebits == z.ebits);   

Reported by: USTCHCS Analysis Toolsuite Bugfinder
(bugfinder-2.3: LHS and RHS of a logical binary-operator (&&, ||), relational/equality binary-operator expression should not contain the same sub-expression.)

[NikolajBjorner]

the bug was reopened but not addressed.

[wintersteiger]

Thanks for the reminder; the check for z.*bits was missing and I was planning to add it back.