Public interface review items:

* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument()
* Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only
* CheckArgument() throws non-AssertionException
* things outside the core library (parsers, driver) use regular C-style assert,
  or a public exception type.
* auto-generated documentation for Smt options and internal options

Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.

1 files changed, 3 insertions, 1 deletions

diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 134498eea..7df2b0210 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -83,7 +83,9 @@ void Tptp::addTheory(Theory theory) {
     break;
 
   default:
-    Unhandled(theory);
+    std::stringstream ss;
+    ss << "internal error: Tptp::addTheory(): unhandled theory " << theory;
+    throw ParserException(ss.str());
   }
 }