google/souper — pull request #139 by rsas (2014-12-15 22:36:35+00:00)
Title: 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.