search

mishun / minisat-rust

Experimental minisat SAT solver reimplementation in Rust
Other
71 stars 6 forks source link

Fix panic in extendModel #1

Closed brohee closed 8 years ago

brohee commented 8 years ago

When j somehow outgrow i in extendModel, we have an underflow and the loop stop condition doesn't work properly. This leads to a panic.

The root cause is i and j being signed in the original C++ code and being usize in the Rust code.

The bug was triggered on 3bitadd_32.cnf from the problem set http://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/Bejing/Bejing.tar.gz

(Found on http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html)

mishun commented 8 years ago

Thanks!