mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Bug/assertion fix for power monomials in nlsat.

Browse source 
Previously triggered an assertion on regressions/smt2/fp-to_real-1.smt2, but only on OSX and FreeBSD
This commit is contained in:
Christoph M. Wintersteiger 2015-09-17 16:31:51 +01:00
parent 05d9e188f8
commit d4b66538f9
1 changed files with 18 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/math/polynomial/polynomial.cpp
View file

@ -99,8 +99,17 @@ namespace polynomial {
void set_var(var x) { first = x; } void set_var(var x) { first = x; }
struct lt_var { struct lt_var {
bool operator()(power const & p1, power const & p2) { bool operator()(power const & p1, power const & p2) {
SASSERT(p1.get_var() != p2.get_var()); // 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(); return p1.get_var() < p2.get_var();
} }
}; };
@ -3242,6 +3251,13 @@ namespace polynomial {
SASSERT(var2pos[pws[i].get_var()] != UINT_MAX); SASSERT(var2pos[pws[i].get_var()] != UINT_MAX);
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) { void var_max_degrees(polynomial const * p, power_buffer & pws) {