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.
In any case it's not clear to me that Souper is guaranteed to process the candidates in any particular order so you shouldn't rely on that.