SMT-LIB Compliance

CVC4 is mostly SMT-LIB-conforming with --lang smt. With the --smtlib command line option, though, you get additional strictness and standards conformance.

There are areas where we don't support full functionality, or where we are not compliant:

• We do not yet support the to_real or to_int functions, nor the is_int predicate, from the Reals_Ints theory.
• We do not yet support unsat core extraction (the get-unsat-core command)
• We do not yet adequately support nonlinear-arithmetic (the QF_NIA, QF_NRA, QF_UFNRA, UFNRA, and AUFNIRA logics)

Also, please note that CVC4 is not intended as a compliance-checker for SMT-LIB input. That is, it is a bit lenient in accepting non-conforming input.