Gl-force-check
When found in an if test, forces GL to check satisfiability of the test.
When using GL's AIG-based modes, it is sometimes important to force
GL to check whether an IF test is constant-true or constant-false. For
example, if the if guards a recursive call, then symbolic
interpretation of the function may diverge if the test isn't checked.
Usage:
(gl-force-check test :strong nil :dir :both)
Here :strong governs whether the path condition is considered; by
default it is not, because it is potentially much more expensive to do the
check when considering the path condition. :dir may be t, nil,
or :both (the default). If t, then we only try to show that
test is constant-true; if nil, we only try to show it constant-false;
if :both, then we try both directions.
