Refactoring

This change adds a single point where that can allow
error descriptor generation to be instrumented easily.
Tweak SAT checking

The general form of queries is

   errorCondition && knownFactsAtLocation

where `errorCondition` is a formula that is true when an
error is being handled.  The idea is to see if that and the facts
in scope are consistent.  If they are, an error is being handled.
The code was not dealing with the case where no (relevant) facts are
known at the current scope.  In those cases, `errorCondition` was
trivially satisfiable, which is not really the desired meaning.

This change fails early (even before SMT) if no facts are known at the
current location.
Remove a stray debug call
Lift the single-predecessor restriction on known-errors

Before, the analysis would not consider blocks with more than one
predecessor.  This was for simplicity, but made us miss some inferences
we should have been able to make.  That is corrected with this change.

Note that the analysis that identifies success codes still has this
restriction.  That could, in principle, be lifted in a similar way.
It may not be necessary, however.
Add a test case for the last change
Fix some missed null-pointer cases

Null pointers were being ignored; this commit now treats them
like ints.  Test included.