Fixed side conditions for CBQI BV, added unit tests. (#1434)

Fixed side conditions for CBQI BV, added unit tests. (#1434)

This fixes the side conditions for BITVECTOR_UREM_TOTAL, BITVECTOR_UDIV_TOTAL,
BITVECTOR_LSHR, BITVECTOR_ASHR, BITVECTOR_SHL.

It refactors side condition generation for better readability and unit testing.
It further adds unit tests for all side conditions we generate in order to check if they too weak
or to restrictive (which may result in unsound behavior).

This is achieved by checking the following two implications:
not (exists x. s * x = t => SC) ... if sat, SC is too restrictive
not (SC => exists x. s * x = t) ... if sat SC is too weak

This simplifies to checking not (SC <=> exists x. s * x = t).