Unit-ness check for learnt clause

[rajdeep87]

The regression branch7 computes the learnt clause with the first-UIP which is not UNIT.
Learnt clause: !(-((signed __CPROVER_bitvector[33])id#return_value#32) >= -1) || !(!(a#31 >= 0))
Comparing relevant expressions !(a#31 >= 3) && !(-((signed __CPROVER_bitvector[33])a#31) >= 2) <---> !(!(a#31 >= 0))
The status is 1
2ls: acdl_analyze_conflict_base.cpp:195: bool acdl_analyze_conflict_baset::operator()(const local_SSAt&, acdl_conflict_grapht&): Assertion `result==3' failed.

Simply, this is checking the value (a>-2 && a<3) with the meet irreducible in the learnt clause which is a>=0. Clearly, this is UNIT.