Unit clauses not propagated again when doing multiple calls to the SAT solver
The issue was described by Axel on SAT4J forum: http://forge.ow2.org/forum/message.php?msg_id=118089
The short story is that unit clauses, after being propagated once, are no longer propagated on successive calls to the SAT solver because qhead was not reset to 0 but to trail.last().