Michael Tautschnig <[email protected]> reports: The problem, at least for most of the build failures, is a very simple one: An endianness issue, which actually lies in the original MiniSat code. The declaration of d_assigns in line 251 of src/sat/minisat_solver.h declares the assignments as a vector of chars; assignments happen using the toInt function from src/sat/minisat_global.h, which returns *an int*. Now a lifted Boolean just requires 2 bits and using a vector of chars may be (depending on memory alignment) less memory consuming, but an implicit cast from this int to char is bound to fail on big-endian systems.
The simplest way to fix this is declaring d_assigns as a vector of ints with a corresponding fix of declarations in minisat_varorder.h; this change, however, could possibly be intrusive memory-wise and you will want to re-run CVC 3 on some SMT Comp instances and compare the performance. If you have to stick with a vector of chars, then a proper wrapper of toInt (e.g., toChar) should be added the behavior of which depends on the architecture. -- To UNSUBSCRIBE, email to [email protected] with a subject of "unsubscribe". Trouble? Contact [email protected]
