SMT-LIB Compliance

From CVC4
Revision as of 09:47, 27 September 2014 by Mdeters (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

CVC4 is mostly SMT-LIB-conforming with --lang smt. With the --smtlib-strict 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 adequately support nonlinear-arithmetic (the QF_NIA, QF_NRA, QF_UFNRA, UFNRA, and AUFNIRA logics)
  • We do not yet support all the features of the recent (September 2014) draft of SMT-LIB 2.5

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.

Retrieved from "http://cvc4.cs.stanford.edu/w/index.php?title=SMT-LIB_Compliance&oldid=5300"