Bug: avoid doing equality comparisons between floating expressions.

[ustchcs-bugfinder]

z3/src/math/dd/dd_bdd.cpp

Line 321 in 8439057

while (current_cost() != best_cost) {

z3/src/math/dd/dd_bdd.cpp

Line 342 in 8439057

while (current_cost() != best_cost) {

Doing equality/inequality judgement on doubles is not a best practice.

There are lots of discussions on stackoverflow.

• https://stackoverflow.com/questions/17404513/floating-point-equality-and-tolerances
• https://stackoverflow.com/questions/9542391/float-double-equality-with-exact-zero

void bdd_manager::sift_var(unsigned v) {
        unsigned lvl = m_var2level[v];
        unsigned start = lvl;
        double best_cost = current_cost();
        ...
            while (current_cost() != best_cost) {    // do equality/inequality judgement on doubles
                sift_up(--lvl);
            }
        ...
        }

Reported by: USTCHCS Analysis Toolsuite Bugfinder
(bugfinder-5.15: Avoid doing equality comparisons between floating expressions.)