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.
I think that in this test case we should check for the optimization only, because the goal of the test case is to test intrinsics.