[bugfix] Attempt at fixing enqueue bug
[bugfix] Attempt at fixing enqueue bug

When we enqueue an atom at level 0, we expect it to stay unconditionally
true whatever happens. However, if it happens that the atom is alrady
true at a level strictly greater than 0 (but lower than base_level),
then enqueue_bool would simply do nothing. To fix this, there is a new
function enqueue_root which modifies in place the level and reason of
the propagated atom if it is already true.
Additionally, enqueue_bool now requires that the atom be undecided,
since if it not (i.e if it is propagated while already decided) it is
most likely a bug.

Gbury/mSAT