This appears to be caused by the following assignment in
src/sat/minisat_solver.cpp, line 1582:
d_assigns[var] = toInt(lbool(p.sign()));
d_assigns has type vector<char>. On the affected architectures, char
is unsigned. When p.sign() is -1, the result is that d_assigns[var] is
assigned 255, an unsigned char, which causes the following assertion
to fail, because the value of l_False is -1, a signed int
(getValue(c[z]) just coerces the d_assigns value for c[z].var() to
int):
DebugAssert(getValue(c[z]) == l_False,
"MiniSat::Solver:::propagate: Unit Propagation");
The offending assignment exists in the upstream MiniSat code, but it's
not clear whether it leads to a bug in the absence of the changes made
for CVC3 (the assertion is one such change).
A simple fix is to change the type of d_assigns to vector<signed
char>. A new version of the package with this fix is pending.
--
To UNSUBSCRIBE, email to debian-bugs-rc-requ...@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org
