Add iN synthesis with two queries (no quantifiers)

This patch teaches Souper to infer iN integers (``-souper-infer-iN`` option) using two solver queries without quantifiers. The first query is a SAT query ``LHS == constant`` asking for a model for ``constant`` whereas the second query is a ``LHS != constant_model`` query. If the result of the latter is UNSAT, we have synthesized a valid integer.

Note that STP doesn't support SMTLIBv2 option ``:produce-models``, so we have to use z3 or cvc4.
``consumeExpected('x', ErrStr)`` on line [183](https://github.com/google/souper/pull/139/files#diff-eec41c673a3d259ad37faf697508f877R183) might fail filling ``ErrStr``. We ignore it and continue to ``parseBinaryBitVector(ErrStr)``