[SMT-LIB] Mixing Integers and Reals in SMT2 formulas

[Martin Brain]

On Fri, 2014-07-18 at 11:16 -0700, Levent Erkok wrote:
> I think the point is that such queries should be rejected by compliant
> solvers. Or, contrapositively, any solver not rejecting such a query is
> non-compliant with the standard. This follows from the core theory
> definition in
> http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r10.12.21.pdf,
> page 30; which requires equality to receive the same "sort" for its
> arguments.

The problem with requiring all compliant solvers to reject non-compliant
input is that it prevents developers adding their own extensions.  As I
understand it, SMT-LIB is written to support authors in further
developing and extending the language.

> This is not a mere academic interest: At least in my use case the SMT
> solver sits at the very end of an already bloated tool chain that generates
> bunch of verification-conditions, rewrites them, modifies it in a variety
> of ways, and finally ships it off to the solver. If I introduce a bug
> somewhere in that tool-chain (quite likely) and thus generate such invalid
> queries, I'd very much like the SMT-solver to simply reject my query
> instead of silently accepting it and doing something with it. I consider
> this a very important, yet oft-overlooked problem, which could have
> implications on the adoption of SMT-solvers in the industry.

Some people are working on jSMTLIB as an official validator for SMT-LIB
2 plus some solvers do have a 'strict' mode.  Perhaps if you ran these
in parallel with you main solver. during development and testing, you
could catch cases where you are generating non-compliant output.  If it
was another solver you could also cross-validate the output to
potentially catch solver bugs.

Cheers,
 - Martin