From d4b66538f93a4e9b255690bf127ffae3f4cc493c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 17 Sep 2015 16:31:51 +0100 Subject: [PATCH] Bug/assertion fix for power monomials in nlsat. Previously triggered an assertion on regressions/smt2/fp-to_real-1.smt2, but only on OSX and FreeBSD --- src/math/polynomial/polynomial.cpp | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 93dc419d8..5599156d5 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -99,8 +99,17 @@ namespace polynomial { void set_var(var x) { first = x; } struct lt_var { - bool operator()(power const & p1, power const & p2) { - SASSERT(p1.get_var() != p2.get_var()); + bool operator()(power const & p1, power const & p2) { + // CMW: The assertion below does not hold on OSX, because + // their implementation of std::sort will try to compare + // two items at the same index instead of comparing + // the indices directly. I suspect that the purpose of + // this assertion was to make sure that there are + // no duplicates, so I replaced it with a new assertion at + // the end of var_degrees(...). + + // SASSERT(p1.get_var() != p2.get_var()); + return p1.get_var() < p2.get_var(); } }; @@ -3242,6 +3251,13 @@ namespace polynomial { SASSERT(var2pos[pws[i].get_var()] != UINT_MAX); var2pos[pws[i].get_var()] = UINT_MAX; } + + DEBUG_CODE({ + for (unsigned i = 0; i < pws.size(); i++) { + for (unsigned j = i + 1; j < pws.size(); j++) + SASSERT(pws[i].first != pws[j].first); + } + }); } void var_max_degrees(polynomial const * p, power_buffer & pws) {