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.

27 files changed, 166 insertions, 153 deletions

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index ea593e7da..0dc833ee5 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -36,7 +36,6 @@
 #include "parser/smt2/smt2_input.h"
 #include "parser/tptp/tptp_input.h"
 #include "util/output.h"
-#include "util/Assert.h"
 
 using namespace std;
 using namespace CVC4;
@@ -51,7 +50,7 @@ AntlrInputStream::AntlrInputStream(std::string name,
                                    bool fileIsTemporary) :
   InputStream(name,fileIsTemporary),
   d_input(input) {
-  AlwaysAssert( input != NULL );
+  assert( input != NULL );
 }
 
 AntlrInputStream::~AntlrInputStream() {
@@ -65,7 +64,7 @@ pANTLR3_INPUT_STREAM AntlrInputStream::getAntlr3InputStream() const {
 AntlrInputStream*
 AntlrInputStream::newFileInputStream(const std::string& name,
                                      bool useMmap)
-  throw (InputStreamException, AssertionException) {
+  throw (InputStreamException) {
   pANTLR3_INPUT_STREAM input = NULL;
   if( useMmap ) {
     input = MemoryMappedInputBufferNew(name);
@@ -87,7 +86,7 @@ AntlrInputStream*
 AntlrInputStream::newStreamInputStream(std::istream& input,
                                        const std::string& name,
                                        bool lineBuffered)
-  throw (InputStreamException, AssertionException) {
+  throw (InputStreamException) {
 
   pANTLR3_INPUT_STREAM inputStream = NULL;
 
@@ -162,10 +161,10 @@ AntlrInputStream::newStreamInputStream(std::istream& input,
 AntlrInputStream*
 AntlrInputStream::newStringInputStream(const std::string& input,
                                        const std::string& name)
-  throw (InputStreamException, AssertionException) {
+  throw (InputStreamException) {
   char* inputStr = strdup(input.c_str());
   char* nameStr = strdup(name.c_str());
-  AlwaysAssert( inputStr!=NULL && nameStr!=NULL );
+  assert( inputStr!=NULL && nameStr!=NULL );
 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
   pANTLR3_INPUT_STREAM inputStream =
       antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8) inputStr,
@@ -207,7 +206,9 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre
     break;
 
   default:
-    Unhandled(lang);
+    std::stringstream ss;
+    ss << "internal error: unhandled language " << lang << " in AntlrInput::newInput";
+    throw ParserException(ss.str());
   }
 
   return input;
@@ -261,11 +262,11 @@ pANTLR3_COMMON_TOKEN_STREAM AntlrInput::getTokenStream() {
 
 void AntlrInput::lexerError(pANTLR3_BASE_RECOGNIZER recognizer) {
   pANTLR3_LEXER lexer = (pANTLR3_LEXER)(recognizer->super);
-  AlwaysAssert(lexer!=NULL);
+  assert(lexer!=NULL);
   Parser *parser = (Parser*)(lexer->super);
-  AlwaysAssert(parser!=NULL);
+  assert(parser!=NULL);
   AntlrInput *input = (AntlrInput*) parser->getInput();
-  AlwaysAssert(input!=NULL);
+  assert(input!=NULL);
 
   /* Call the error display routine *if* there's not already a 
    * parse error pending.  If a parser error is pending, this
@@ -280,7 +281,7 @@ void AntlrInput::warning(const std::string& message) {
 }
 
 void AntlrInput::parseError(const std::string& message)
-  throw (ParserException, AssertionException) {
+  throw (ParserException) {
   Debug("parser") << "Throwing exception: "
       << getInputStream()->getName() << ":"
       << d_lexer->getLine(d_lexer) << "."
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 2d468a7d6..613390ca1 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -27,12 +27,12 @@
 #include <stdexcept>
 #include <string>
 #include <vector>
+#include <cassert>
 
 #include "parser/bounded_token_buffer.h"
 #include "parser/parser_exception.h"
 #include "parser/input.h"
 
-#include "util/Assert.h"
 #include "util/bitvector.h"
 #include "util/integer.h"
 #include "util/rational.h"
@@ -73,13 +73,13 @@ public:
    */
   static AntlrInputStream* newFileInputStream(const std::string& name, 
                                               bool useMmap = false)
-    throw (InputStreamException, AssertionException);
+    throw (InputStreamException);
 
   /** Create an input from an istream. */
   static AntlrInputStream* newStreamInputStream(std::istream& input, 
                                                 const std::string& name,
                                                 bool lineBuffered = false)
-    throw (InputStreamException, AssertionException);
+    throw (InputStreamException);
 
   /** Create a string input.
    *
@@ -88,7 +88,7 @@ public:
    */
   static AntlrInputStream* newStringInputStream(const std::string& input, 
                                                 const std::string& name)
-    throw (InputStreamException, AssertionException);
+    throw (InputStreamException);
 };/* class AntlrInputStream */
 
 class Parser;
@@ -212,7 +212,7 @@ protected:
    * Throws a <code>ParserException</code> with the given message.
    */
   void parseError(const std::string& msg)
-    throw (ParserException, AssertionException);
+    throw (ParserException);
 
   /** Set the ANTLR3 lexer for this input. */
   void setAntlr3Lexer(pANTLR3_LEXER pLexer);
@@ -255,7 +255,7 @@ inline std::string AntlrInput::tokenTextSubstr(pANTLR3_COMMON_TOKEN token,
   ANTLR3_MARKER start = token->getStartIndex(token);
   // Its the last character of the token (not the one just after)
   ANTLR3_MARKER end = token->getStopIndex(token);
-  Assert( start < end );
+  assert( start < end );
   if( index > (size_t) end - start ) {
     std::stringstream ss;
     ss << "Out-of-bounds substring index: " << index;
diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp
index d714c4975..9c92846bb 100644
--- a/src/parser/antlr_input_imports.cpp
+++ b/src/parser/antlr_input_imports.cpp
@@ -57,7 +57,6 @@
 #include "parser/antlr_input.h"
 #include "parser/parser.h"
 #include "parser/parser_exception.h"
-#include "util/Assert.h"
 
 using namespace std;
 
@@ -92,11 +91,11 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
 
   // Dig the CVC4 objects out of the ANTLR3 mess
   pANTLR3_PARSER antlr3Parser = (pANTLR3_PARSER)(recognizer->super);
-  AlwaysAssert(antlr3Parser!=NULL);
+  assert(antlr3Parser!=NULL);
   Parser *parser = (Parser*)(antlr3Parser->super);
-  AlwaysAssert(parser!=NULL);
+  assert(parser!=NULL);
   AntlrInput *input = (AntlrInput*) parser->getInput() ;
-  AlwaysAssert(input!=NULL);
+  assert(input!=NULL);
 
   // Signal we are in error recovery now
   recognizer->state->errorRecovery = ANTLR3_TRUE;
@@ -235,7 +234,7 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
         }
       }
     } else {
-      Unreachable("Parse error with empty set of expected tokens.");
+      assert(false);//("Parse error with empty set of expected tokens.");
     }
   }
     break;
@@ -257,7 +256,7 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
     // then we are just going to report what we know about the
     // token.
     //
-    Unhandled("Unexpected exception in parser.");
+    assert(false);//("Unexpected exception in parser.");
     break;
   }
 
diff --git a/src/parser/antlr_line_buffered_input.cpp b/src/parser/antlr_line_buffered_input.cpp
index b42562f72..0facbddaf 100644
--- a/src/parser/antlr_line_buffered_input.cpp
+++ b/src/parser/antlr_line_buffered_input.cpp
@@ -20,9 +20,9 @@
 #include <antlr3.h>
 #include <iostream>
 #include <string>
+#include <cassert>
 
 #include "util/output.h"
-#include "util/Assert.h"
 
 namespace CVC4 {
 namespace parser {
@@ -242,7 +242,7 @@ myLA(pANTLR3_INT_STREAM is, ANTLR3_INT32 la) {
         in.getline((((char*)input->data) + input->sizeBuf), 1024);
       }
       input->sizeBuf += strlen(((char*)input->data) + input->sizeBuf);
-      Assert(*(((char*)input->data) + input->sizeBuf) == '\0');
+      assert(*(((char*)input->data) + input->sizeBuf) == '\0');
       Debug("pipe") << "SIZEBUF now " << input->sizeBuf << std::endl;
       *(((char*)input->data) + input->sizeBuf) = '\n';
       ++input->sizeBuf;
diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp
index d63d3afe0..7edbf7b7f 100644
--- a/src/parser/bounded_token_buffer.cpp
+++ b/src/parser/bounded_token_buffer.cpp
@@ -56,7 +56,7 @@
 #include <antlr3tokenstream.h>
 
 #include "parser/bounded_token_buffer.h"
-#include "util/Assert.h"
+#include <cassert>
 
 namespace CVC4 {
 namespace parser {
@@ -142,7 +142,7 @@ BoundedTokenBufferSourceNew(ANTLR3_UINT32 k, pANTLR3_TOKEN_SOURCE source)
     pANTLR3_COMMON_TOKEN_STREAM	stream;
 
 
-    AlwaysAssert( k > 0 );
+    assert( k > 0 );
 
     /* Memory for the interface structure
      */
@@ -235,7 +235,7 @@ static pANTLR3_COMMON_TOKEN tokLT(pANTLR3_TOKEN_STREAM ts, ANTLR3_INT32 k) {
   buffer = (pBOUNDED_TOKEN_BUFFER) cts->super;
 
   /* k must be in the range [-buffer->k..buffer->k] */
-  AlwaysAssert( k <= (ANTLR3_INT32)buffer->k 
+  assert( k <= (ANTLR3_INT32)buffer->k 
                 && -k <= (ANTLR3_INT32)buffer->k );
 
   if(k == 0) {
@@ -244,7 +244,7 @@ static pANTLR3_COMMON_TOKEN tokLT(pANTLR3_TOKEN_STREAM ts, ANTLR3_INT32 k) {
 
   /* Initialize the buffer on our first call. */
   if( EXPECT_FALSE(buffer->empty == ANTLR3_TRUE) ) {
-    AlwaysAssert( buffer->tokenBuffer != NULL );
+    assert( buffer->tokenBuffer != NULL );
     buffer->tokenBuffer[ 0 ] = nextToken(buffer);
     buffer->maxIndex = 0;
     buffer->currentIndex = 0;
@@ -257,7 +257,7 @@ static pANTLR3_COMMON_TOKEN tokLT(pANTLR3_TOKEN_STREAM ts, ANTLR3_INT32 k) {
     kIndex = buffer->currentIndex + k - 1;
   } else {
     /* Can't look behind more tokens than we've consumed. */
-    AlwaysAssert( -k <= (ANTLR3_INT32)buffer->currentIndex );
+    assert( -k <= (ANTLR3_INT32)buffer->currentIndex );
     /* look-behind token k is at offset -k */
     kIndex = buffer->currentIndex + k;
   }
@@ -289,7 +289,8 @@ dbgTokLT  (pANTLR3_TOKEN_STREAM ts, ANTLR3_INT32 k)
 static pANTLR3_COMMON_TOKEN 
 get (pANTLR3_TOKEN_STREAM ts, ANTLR3_UINT32 i)
 {
-  Unreachable();
+    assert(false);// unimplemented
+    return NULL;
 }
 
 static pANTLR3_TOKEN_SOURCE 
@@ -308,19 +309,22 @@ setTokenSource	(   pANTLR3_TOKEN_STREAM ts,
 static pANTLR3_STRING	    
 toString    (pANTLR3_TOKEN_STREAM ts)
 {
-  Unimplemented("toString(ts)");
+  assert(false);// unimplemented
+  return NULL;
 }
 
 static pANTLR3_STRING
 toStringSS(pANTLR3_TOKEN_STREAM ts, ANTLR3_UINT32 start, ANTLR3_UINT32 stop)
 {
-  Unimplemented("toStringSS(ts, %u, %u)", start, stop);
+  assert(false);// unimplemented
+  return NULL;
 }
 
 static pANTLR3_STRING	    
 toStringTT  (pANTLR3_TOKEN_STREAM ts, pANTLR3_COMMON_TOKEN start, pANTLR3_COMMON_TOKEN stop)
 {
-  Unimplemented("toStringTT(ts, %u, %u)", start, stop);
+  assert(false);// unimplemented
+  return NULL;
 }
 
 /** Move the input pointer to the next incoming token.  The stream
@@ -379,7 +383,8 @@ _LA  (pANTLR3_INT_STREAM is, ANTLR3_INT32 i)
 static ANTLR3_UINT32	    
 dbgLA  (pANTLR3_INT_STREAM is, ANTLR3_INT32 i)
 {
-  Unreachable();
+  assert(false);
+  return 0;
 }
 
 static ANTLR3_MARKER
@@ -394,7 +399,8 @@ mark	(pANTLR3_INT_STREAM is)
 static ANTLR3_MARKER
 dbgMark	(pANTLR3_INT_STREAM is)
 {
-  Unreachable();
+  assert(false);
+  return 0;
 }
 
 static void		    
@@ -406,7 +412,8 @@ release	(pANTLR3_INT_STREAM is, ANTLR3_MARKER mark)
 static ANTLR3_UINT32	    
 size	(pANTLR3_INT_STREAM is)
 {
-  Unreachable();
+  assert(false);
+  return 0;
 }
 
 static ANTLR3_MARKER   
@@ -426,12 +433,12 @@ tindex	(pANTLR3_INT_STREAM is)
 static void		    
 dbgRewindLast	(pANTLR3_INT_STREAM is)
 {
-  Unreachable();
+  assert(false);
 }
 static void		    
 rewindLast	(pANTLR3_INT_STREAM is)
 {
-  Unreachable();
+  assert(false);
 }
 static void		    
 rewindStream	(pANTLR3_INT_STREAM is, ANTLR3_MARKER marker)
@@ -441,7 +448,7 @@ rewindStream	(pANTLR3_INT_STREAM is, ANTLR3_MARKER marker)
 static void		    
 dbgRewindStream	(pANTLR3_INT_STREAM is, ANTLR3_MARKER marker)
 {
-   Unreachable();
+   assert(false);
 }
 
 static void		    
@@ -458,7 +465,7 @@ seek	(pANTLR3_INT_STREAM is, ANTLR3_MARKER index)
 static void		    
 dbgSeek	(pANTLR3_INT_STREAM is, ANTLR3_MARKER index)
 {
-  Unreachable();
+  assert(false);
 }
 
 static pANTLR3_COMMON_TOKEN nextToken(pBOUNDED_TOKEN_BUFFER buffer) {
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 4577b504c..b496aa91c 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -288,7 +288,9 @@ int getOperatorPrecedence(int type) {
   case IN_TOK: return 33;
 
   default:
-    Unhandled(CvcParserTokenNames[type]);
+    std::stringstream ss;
+    ss << "internal error: no entry in precedence table for operator " << CvcParserTokenNames[type];
+    throw ParserException(ss.str());
   }
 }/* getOperatorPrecedence() */
 
@@ -318,16 +320,18 @@ Kind getOperatorKind(int type, bool& negate) {
   case INTDIV_TOK: return kind::INTS_DIVISION;
   case MOD_TOK: return kind::INTS_MODULUS;
   case DIV_TOK: return kind::DIVISION;
-  case EXP_TOK: Unhandled(CvcParserTokenNames[type]);
+  case EXP_TOK: break;
 
     // bvBinop
   case CONCAT_TOK: return kind::BITVECTOR_CONCAT;
   case BAR: return kind::BITVECTOR_OR;
   case BVAND_TOK: return kind::BITVECTOR_AND;
-
-  default:
-    Unhandled(CvcParserTokenNames[type]);
   }
+
+  std::stringstream ss;
+  ss << "internal error: no entry in operator-kind table for operator " << CvcParserTokenNames[type];
+  throw ParserException(ss.str());
+
 }/* getOperatorKind() */
 
 unsigned findPivot(const std::vector<unsigned>& operators,
@@ -355,10 +359,10 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em,
                           const std::vector<CVC4::Expr>& expressions,
                           const std::vector<unsigned>& operators,
                           unsigned startIndex, unsigned stopIndex) {
-  Assert(expressions.size() == operators.size() + 1);
-  Assert(startIndex < expressions.size());
-  Assert(stopIndex < expressions.size());
-  Assert(startIndex <= stopIndex);
+  assert(expressions.size() == operators.size() + 1);
+  assert(startIndex < expressions.size());
+  assert(stopIndex < expressions.size());
+  assert(startIndex <= stopIndex);
 
   if(stopIndex == startIndex) {
     return expressions[startIndex];
@@ -450,6 +454,7 @@ Expr addNots(ExprManager* em, size_t n, Expr e) {
 @parser::includes {
 
 #include <stdint.h>
+#include <cassert>
 #include "expr/command.h"
 #include "parser/parser.h"
 #include "util/subrange_bound.h"
@@ -1016,7 +1021,7 @@ type[CVC4::Type& t,
     /* a type, possibly a function */
   : restrictedTypePossiblyFunctionLHS[t,check,lhs]
     { if(lhs) {
-        Assert(t.isTuple());
+        assert(t.isTuple());
         args = TupleType(t).getTypes();
       } else {
         args.push_back(t);
@@ -1430,7 +1435,7 @@ arrayStore[CVC4::Expr& f]
 }
   : ( LBRACKET formula[f2] { dims.push_back(f2); } RBRACKET )+
     ASSIGN_TOK uminusTerm[f3]
-    { Assert(dims.size() >= 1);
+    { assert(dims.size() >= 1);
       // these loops are a bit complicated; they're only used for the
       // multidimensional ...WITH [a][b] :=... syntax
       for(unsigned i = 0; i < dims.size() - 1; ++i) {
@@ -1630,7 +1635,7 @@ postfixTerm[CVC4::Expr& f]
         } else if(t.isTester()) {
           f = MK_EXPR(CVC4::kind::APPLY_TESTER, args);
         } else {
-          Unhandled(t);
+          PARSER_STATE->parseError("internal error: unhandled function application kind");
         }
       }
 
@@ -1864,18 +1869,18 @@ simpleTerm[CVC4::Expr& f]
   | INTEGER_LITERAL { f = MK_CONST(AntlrInput::tokenToInteger($INTEGER_LITERAL)); }
     /* bitvector literals */
   | HEX_LITERAL
-    { Assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 );
+    { assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 );
       std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 4);
       f = MK_CONST( BitVector(hexString, 16) ); }
   | BINARY_LITERAL
-    { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 );
+    { assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 );
       std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 4);
       f = MK_CONST( BitVector(binString, 2) ); }
     /* record literals */
   | PARENHASH recordEntry[name,e] { names.push_back(name); args.push_back(e); }
     ( COMMA recordEntry[name,e] { names.push_back(name); args.push_back(e); } )* HASHPAREN
     { std::vector< std::pair<std::string, Type> > typeIds;
-      Assert(names.size() == args.size());
+      assert(names.size() == args.size());
       for(unsigned i = 0; i < names.size(); ++i) {
         typeIds.push_back(std::make_pair(names[i], args[i].getType()));
       }
diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp
index d91a13bee..26ee4a693 100644
--- a/src/parser/cvc/cvc_input.cpp
+++ b/src/parser/cvc/cvc_input.cpp
@@ -32,7 +32,7 @@ namespace parser {
 CvcInput::CvcInput(AntlrInputStream& inputStream) :
   AntlrInput(inputStream,6) {
   pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
-  AlwaysAssert( input != NULL );
+  assert( input != NULL );
 
   d_pCvcLexer = CvcLexerNew(input);
   if( d_pCvcLexer == NULL ) {
@@ -42,7 +42,7 @@ CvcInput::CvcInput(AntlrInputStream& inputStream) :
   setAntlr3Lexer( d_pCvcLexer->pLexer );
 
   pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
-  AlwaysAssert( tokenStream != NULL );
+  assert( tokenStream != NULL );
 
   d_pCvcParser = CvcParserNew(tokenStream);
   if( d_pCvcParser == NULL ) {
@@ -59,12 +59,12 @@ CvcInput::~CvcInput() {
 }
 
 Command* CvcInput::parseCommand()
-  throw (ParserException, TypeCheckingException, AssertionException) {
+  throw (ParserException, TypeCheckingException) {
   return d_pCvcParser->parseCommand(d_pCvcParser);
 }
 
 Expr CvcInput::parseExpr()
-  throw (ParserException, TypeCheckingException, AssertionException) {
+  throw (ParserException, TypeCheckingException) {
   return d_pCvcParser->parseExpr(d_pCvcParser);
 }
 
diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h
index 9a1f24fde..94e1bfc60 100644
--- a/src/parser/cvc/cvc_input.h
+++ b/src/parser/cvc/cvc_input.h
@@ -66,7 +66,7 @@ protected:
    * @throws ParserException if an error is encountered during parsing.
    */
   Command* parseCommand() 
-    throw(ParserException, TypeCheckingException, AssertionException);
+    throw(ParserException, TypeCheckingException);
 
   /** Parse an expression from the input. Returns a null <code>Expr</code>
    * if there is no expression there to parse.
@@ -74,7 +74,7 @@ protected:
    * @throws ParserException if an error is encountered during parsing.
    */
   Expr parseExpr() 
-    throw(ParserException, TypeCheckingException, AssertionException);
+    throw(ParserException, TypeCheckingException);
 
 private:
 
diff --git a/src/parser/input.cpp b/src/parser/input.cpp
index 76aa47812..12c674a61 100644
--- a/src/parser/input.cpp
+++ b/src/parser/input.cpp
@@ -24,7 +24,6 @@
 #include "expr/type.h"
 #include "parser/antlr_input.h"
 #include "util/output.h"
-#include "util/Assert.h"
 
 using namespace std;
 using namespace CVC4;
@@ -57,7 +56,7 @@ InputStream *Input::getInputStream() {
 Input* Input::newFileInput(InputLanguage lang,
                            const std::string& filename,
                            bool useMmap)
-  throw (InputStreamException, AssertionException) {
+  throw (InputStreamException) {
   AntlrInputStream *inputStream = 
     AntlrInputStream::newFileInputStream(filename, useMmap);
   return AntlrInput::newInput(lang, *inputStream);
@@ -67,7 +66,7 @@ Input* Input::newStreamInput(InputLanguage lang,
                              std::istream& input, 
                              const std::string& name,
                              bool lineBuffered)
-  throw (InputStreamException, AssertionException) {
+  throw (InputStreamException) {
   AntlrInputStream *inputStream = 
     AntlrInputStream::newStreamInputStream(input, name, lineBuffered);
   return AntlrInput::newInput(lang, *inputStream);
@@ -76,7 +75,7 @@ Input* Input::newStreamInput(InputLanguage lang,
 Input* Input::newStringInput(InputLanguage lang,
                              const std::string& str,
                              const std::string& name)
-  throw (InputStreamException, AssertionException) {
+  throw (InputStreamException) {
   AntlrInputStream *inputStream = AntlrInputStream::newStringInputStream(str, name);
   return AntlrInput::newInput(lang, *inputStream);
 }
diff --git a/src/parser/input.h b/src/parser/input.h
index d47ca4d12..6f30724d1 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -29,7 +29,6 @@
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "parser/parser_exception.h"
-#include "util/Assert.h"
 #include "util/language.h"
 
 namespace CVC4 {
@@ -111,7 +110,7 @@ public:
   static Input* newFileInput(InputLanguage lang,
                              const std::string& filename,
                              bool useMmap = false)
-    throw (InputStreamException, AssertionException);
+    throw (InputStreamException);
 
   /** Create an input for the given stream.
    *
@@ -126,7 +125,7 @@ public:
                                std::istream& input,
                                const std::string& name,
                                bool lineBuffered = false)
-    throw (InputStreamException, AssertionException);
+    throw (InputStreamException);
 
   /** Create an input for the given string
    *
@@ -137,7 +136,7 @@ public:
   static Input* newStringInput(InputLanguage lang,
                                const std::string& input,
                                const std::string& name)
-    throw (InputStreamException, AssertionException);
+    throw (InputStreamException);
 
 
   /** Destructor. Frees the input stream and closes the input. */
@@ -172,7 +171,7 @@ protected:
    * @throws ParserException if an error is encountered during parsing.
    */
   virtual Command* parseCommand()
-    throw (ParserException, TypeCheckingException, AssertionException) = 0;
+    throw (ParserException, TypeCheckingException) = 0;
 
   /**
    * Issue a warning to the user, with source file, line, and column info.
@@ -183,7 +182,7 @@ protected:
    * Throws a <code>ParserException</code> with the given message.
    */
   virtual void parseError(const std::string& msg)
-    throw (ParserException, AssertionException) = 0;
+    throw (ParserException) = 0;
 
   /** Parse an expression from the input by invoking the
    * implementation-specific parsing method. Returns a null
@@ -192,7 +191,7 @@ protected:
    * @throws ParserException if an error is encountered during parsing.
    */
   virtual Expr parseExpr()
-    throw (ParserException, TypeCheckingException, AssertionException) = 0;
+    throw (ParserException, TypeCheckingException) = 0;
 
   /** Set the Parser object for this input. */
   virtual void setParser(Parser& parser) = 0;
diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp
index f0b7a9d2c..8f8f07099 100644
--- a/src/parser/memory_mapped_input_buffer.cpp
+++ b/src/parser/memory_mapped_input_buffer.cpp
@@ -26,7 +26,6 @@
 #include <antlr3input.h>
 
 #include "parser/memory_mapped_input_buffer.h"
-#include "util/Assert.h"
 #include "util/exception.h"
 
 namespace CVC4 {
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 2a64d122d..7b58ba4f9 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -20,6 +20,7 @@
 #include <fstream>
 #include <iterator>
 #include <stdint.h>
+#include <cassert>
 
 #include "parser/input.h"
 #include "parser/parser.h"
@@ -30,7 +31,6 @@
 #include "expr/type.h"
 #include "util/output.h"
 #include "options/options.h"
-#include "util/Assert.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -53,16 +53,15 @@ Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool par
 
 Expr Parser::getSymbol(const std::string& name, SymbolType type) {
   checkDeclaration(name, CHECK_DECLARED, type);
-  Assert( isDeclared(name, type) );
+  assert( isDeclared(name, type) );
 
-  switch( type ) {
-
-  case SYM_VARIABLE: // Functions share var namespace
+  if(type == SYM_VARIABLE) {
+    // Functions share var namespace
     return d_symtab->lookup(name);
-
-  default:
-    Unhandled(type);
   }
+
+  assert(false);//Unhandled(type);
+  return Expr();
 }
 
 
@@ -77,14 +76,14 @@ Expr Parser::getFunction(const std::string& name) {
 Type Parser::getType(const std::string& var_name,
                      SymbolType type) {
   checkDeclaration(var_name, CHECK_DECLARED, type);
-  Assert( isDeclared(var_name, type) );
+  assert( isDeclared(var_name, type) );
   Type t = getSymbol(var_name, type).getType();
   return t;
 }
 
 Type Parser::getSort(const std::string& name) {
   checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
-  Assert( isDeclared(name, SYM_SORT) );
+  assert( isDeclared(name, SYM_SORT) );
   Type t = d_symtab->lookupType(name);
   return t;
 }
@@ -92,14 +91,14 @@ Type Parser::getSort(const std::string& name) {
 Type Parser::getSort(const std::string& name,
                      const std::vector<Type>& params) {
   checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
-  Assert( isDeclared(name, SYM_SORT) );
+  assert( isDeclared(name, SYM_SORT) );
   Type t = d_symtab->lookupType(name, params);
   return t;
 }
 
 size_t Parser::getArity(const std::string& sort_name){
   checkDeclaration(sort_name, CHECK_DECLARED, SYM_SORT);
-  Assert( isDeclared(sort_name, SYM_SORT) );
+  assert( isDeclared(sort_name, SYM_SORT) );
   return d_symtab->lookupArity(sort_name);
 }
 
@@ -187,20 +186,20 @@ Parser::defineVar(const std::string& name, const Expr& val,
                   bool levelZero) {
   Debug("parser") << "defineVar( " << name << " := " << val << " , " << levelZero << ")" << std::endl;;
   d_symtab->bind(name, val, levelZero);
-  Assert( isDeclared(name) );
+  assert( isDeclared(name) );
 }
 
 void
 Parser::defineFunction(const std::string& name, const Expr& val,
                        bool levelZero) {
   d_symtab->bindDefinedFunction(name, val, levelZero);
-  Assert( isDeclared(name) );
+  assert( isDeclared(name) );
 }
 
 void
 Parser::defineType(const std::string& name, const Type& type) {
   d_symtab->bindType(name, type);
-  Assert( isDeclared(name, SYM_SORT) );
+  assert( isDeclared(name, SYM_SORT) );
 }
 
 void
@@ -208,7 +207,7 @@ Parser::defineType(const std::string& name,
                    const std::vector<Type>& params,
                    const Type& type) {
   d_symtab->bindType(name, params, type);
-  Assert( isDeclared(name, SYM_SORT) );
+  assert( isDeclared(name, SYM_SORT) );
 }
 
 void
@@ -283,7 +282,7 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
   std::vector<DatatypeType> types =
     d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
 
-  Assert(datatypes.size() == types.size());
+  assert(datatypes.size() == types.size());
 
   for(unsigned i = 0; i < datatypes.size(); ++i) {
     DatatypeType t = types[i];
@@ -379,9 +378,9 @@ bool Parser::isDeclared(const std::string& name, SymbolType type) {
     return d_symtab->isBound(name);
   case SYM_SORT:
     return d_symtab->isBoundType(name);
-  default:
-    Unhandled(type);
   }
+  assert(false);//Unhandled(type);
+  return false;
 }
 
 void Parser::checkDeclaration(const std::string& varName,
@@ -411,7 +410,7 @@ void Parser::checkDeclaration(const std::string& varName,
     break;
 
   default:
-    Unhandled(check);
+    assert(false);//Unhandled(check);
   }
 }
 
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 7efc4d78c..deeff5a62 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -24,6 +24,7 @@
 #include <string>
 #include <set>
 #include <list>
+#include <cassert>
 
 #include "parser/input.h"
 #include "parser/parser_exception.h"
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 73c31f578..f48d1e309 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -61,29 +61,27 @@ void ParserBuilder::init(ExprManager* exprManager,
 }
 
 Parser* ParserBuilder::build()
-  throw (InputStreamException, AssertionException) {
+  throw (InputStreamException) {
   Input* input = NULL;
   switch( d_inputType ) {
   case FILE_INPUT:
     input = Input::newFileInput(d_lang, d_filename, d_mmap);
     break;
   case LINE_BUFFERED_STREAM_INPUT:
-    AlwaysAssert( d_streamInput != NULL,
-                  "Uninitialized stream input in ParserBuilder::build()" );
+    assert( d_streamInput != NULL );
     input = Input::newStreamInput(d_lang, *d_streamInput, d_filename, true);
     break;
   case STREAM_INPUT:
-    AlwaysAssert( d_streamInput != NULL,
-                  "Uninitialized stream input in ParserBuilder::build()" );
+    assert( d_streamInput != NULL );
     input = Input::newStreamInput(d_lang, *d_streamInput, d_filename);
     break;
   case STRING_INPUT:
     input = Input::newStringInput(d_lang, d_stringInput, d_filename);
     break;
-  default:
-    Unreachable();
   }
 
+  assert(input != NULL);
+
   Parser* parser = NULL;
   switch(d_lang) {
   case language::input::LANG_SMTLIB_V1:
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 095769ab5..4952f310d 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -91,7 +91,7 @@ public:
                 const Options& options);
 
   /** Build the parser, using the current settings. */
-  Parser *build() throw (InputStreamException, AssertionException);
+  Parser *build() throw (InputStreamException);
 
   /** Should semantic checks be enabled in the parser? (Default: yes) */
   ParserBuilder& withChecks(bool flag = true);
diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g
index b228fb9ec..e093037eb 100644
--- a/src/parser/smt1/Smt1.g
+++ b/src/parser/smt1/Smt1.g
@@ -241,7 +241,7 @@ annotatedFormula[CVC4::Expr& expr]
     { if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) {
         /* Unary AND/OR can be replaced with the argument.
 	       It just so happens expr should already by the only argument. */
-        Assert( expr == args[0] );
+        assert( expr == args[0] );
       } else if( CVC4::kind::isAssociative(kind) &&
                  args.size() > EXPR_MANAGER->maxArity(kind) ) {
     	/* Special treatment for associative operators with lots of children */
@@ -474,7 +474,7 @@ functionDeclaration[CVC4::Command*& smt_command]
     { sorts.push_back(t); }
       sortList[sorts] RPAREN_TOK
     { if( sorts.size() == 1 ) {
-        Assert( t == sorts[0] );
+        assert( t == sorts[0] );
       } else {
         t = EXPR_MANAGER->mkFunctionType(sorts);
       }
@@ -566,8 +566,8 @@ annotation[CVC4::Command*& smt_command]
   : attribute[key]
     ( USER_VALUE
       { std::string value = AntlrInput::tokenText($USER_VALUE);
-        Assert(*value.begin() == '{');
-        Assert(*value.rbegin() == '}');
+        assert(*value.begin() == '{');
+        assert(*value.rbegin() == '}');
         // trim whitespace
         value.erase(value.begin(), value.begin() + 1);
         value.erase(value.begin(), std::find_if(value.begin(), value.end(), std::not1(std::ptr_fun<int, int>(std::isspace))));
diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp
index c91743226..9074cc20a 100644
--- a/src/parser/smt1/smt1.cpp
+++ b/src/parser/smt1/smt1.cpp
@@ -117,9 +117,10 @@ void Smt1::addTheory(Theory theory) {
   }
 
   case THEORY_BITVECTOR_ARRAYS_EX: {
-    Unimplemented("Cannot yet handle SMT-LIBv1 bitvector arrays (i.e., the BitVector_ArraysEx theory)");
-    //addOperator(kind::SELECT);
-    //addOperator(kind::STORE);
+    // We don't define the "Array" symbol in this case;
+    // the parser creates the Array[m:n] types on the fly.
+    addOperator(kind::SELECT);
+    addOperator(kind::STORE);
     break;
   }
 
@@ -134,7 +135,6 @@ void Smt1::addTheory(Theory theory) {
   case THEORY_INT_ARRAYS:
   case THEORY_INT_ARRAYS_EX: {
     defineType("Array", getExprManager()->mkArrayType(getExprManager()->integerType(), getExprManager()->integerType()));
-
     addOperator(kind::SELECT);
     addOperator(kind::STORE);
     break;
@@ -167,7 +167,9 @@ void Smt1::addTheory(Theory theory) {
     break;
 
   default:
-    Unhandled(theory);
+    std::stringstream ss;
+    ss << "internal error: unsupported theory " << theory;
+    throw ParserException(ss.str());
   }
 }
 
@@ -229,8 +231,8 @@ void Smt1::setLogic(const std::string& name) {
     addTheory(THEORY_BITVECTORS);
     break;
 
-  case QF_ABV:
-    addTheory(THEORY_ARRAYS_EX);
+  case QF_ABV:// nonstandard logic
+    addTheory(THEORY_BITVECTOR_ARRAYS_EX);
     addTheory(THEORY_BITVECTORS);
     break;
 
@@ -241,18 +243,18 @@ void Smt1::setLogic(const std::string& name) {
 
   case QF_AUFBV:
     addOperator(kind::APPLY_UF);
-    addTheory(THEORY_ARRAYS_EX);
+    addTheory(THEORY_BITVECTOR_ARRAYS_EX);
     addTheory(THEORY_BITVECTORS);
     break;
 
-  case QF_AUFBVLIA:
+  case QF_AUFBVLIA:// nonstandard logic
     addOperator(kind::APPLY_UF);
     addTheory(THEORY_ARRAYS_EX);
     addTheory(THEORY_BITVECTORS);
     addTheory(THEORY_INTS);
     break;
 
-  case QF_AUFBVLRA:
+  case QF_AUFBVLRA:// nonstandard logic
     addOperator(kind::APPLY_UF);
     addTheory(THEORY_ARRAYS_EX);
     addTheory(THEORY_BITVECTORS);
@@ -260,22 +262,22 @@ void Smt1::setLogic(const std::string& name) {
     break;
 
   case QF_AUFLIA:
-    addTheory(THEORY_INT_ARRAYS_EX);
+    addTheory(THEORY_INT_ARRAYS_EX);// nonstandard logic
     addOperator(kind::APPLY_UF);
     addTheory(THEORY_INTS);
     break;
 
-  case QF_AUFLIRA:
+  case QF_AUFLIRA:// nonstandard logic
     addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX);
     addOperator(kind::APPLY_UF);
     addTheory(THEORY_INTS);
     addTheory(THEORY_REALS);
     break;
 
-  case ALL_SUPPORTED:
+  case ALL_SUPPORTED:// nonstandard logic
     addTheory(THEORY_QUANTIFIERS);
     /* fall through */
-  case QF_ALL_SUPPORTED:
+  case QF_ALL_SUPPORTED:// nonstandard logic
     addTheory(THEORY_ARRAYS_EX);
     addOperator(kind::APPLY_UF);
     addTheory(THEORY_INTS);
diff --git a/src/parser/smt1/smt1_input.cpp b/src/parser/smt1/smt1_input.cpp
index 4987cd793..aae990311 100644
--- a/src/parser/smt1/smt1_input.cpp
+++ b/src/parser/smt1/smt1_input.cpp
@@ -33,7 +33,7 @@ namespace parser {
 Smt1Input::Smt1Input(AntlrInputStream& inputStream) :
   AntlrInput(inputStream, 2) {
   pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
-  AlwaysAssert( input != NULL );
+  assert( input != NULL );
 
   d_pSmt1Lexer = Smt1LexerNew(input);
   if( d_pSmt1Lexer == NULL ) {
@@ -43,7 +43,7 @@ Smt1Input::Smt1Input(AntlrInputStream& inputStream) :
   setAntlr3Lexer( d_pSmt1Lexer->pLexer );
 
   pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
-  AlwaysAssert( tokenStream != NULL );
+  assert( tokenStream != NULL );
 
   d_pSmt1Parser = Smt1ParserNew(tokenStream);
   if( d_pSmt1Parser == NULL ) {
@@ -60,12 +60,12 @@ Smt1Input::~Smt1Input() {
 }
 
 Command* Smt1Input::parseCommand()
-  throw (ParserException, TypeCheckingException, AssertionException) {
+  throw (ParserException, TypeCheckingException) {
   return d_pSmt1Parser->parseCommand(d_pSmt1Parser);
 }
 
 Expr Smt1Input::parseExpr()
-  throw (ParserException, TypeCheckingException, AssertionException) {
+  throw (ParserException, TypeCheckingException) {
   return d_pSmt1Parser->parseExpr(d_pSmt1Parser);
 }
 
diff --git a/src/parser/smt1/smt1_input.h b/src/parser/smt1/smt1_input.h
index 77d6f4b50..0f8a962ba 100644
--- a/src/parser/smt1/smt1_input.h
+++ b/src/parser/smt1/smt1_input.h
@@ -69,7 +69,7 @@ protected:
    * @throws ParserException if an error is encountered during parsing.
    */
   Command* parseCommand()
-    throw(ParserException, TypeCheckingException, AssertionException);
+    throw(ParserException, TypeCheckingException);
 
   /**
    * Parse an expression from the input. Returns a null
@@ -78,7 +78,7 @@ protected:
    * @throws ParserException if an error is encountered during parsing.
    */
   Expr parseExpr()
-    throw(ParserException, TypeCheckingException, AssertionException);
+    throw(ParserException, TypeCheckingException);
 
 private:
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index fb97d5d1e..1b778f87a 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -587,7 +587,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
           args.size() == 1) {
         /* Unary AND/OR can be replaced with the argument.
 	       It just so happens expr should already by the only argument. */
-        Assert( expr == args[0] );
+        assert( expr == args[0] );
       } else if( CVC4::kind::isAssociative(kind) &&
                  args.size() > EXPR_MANAGER->maxArity(kind) ) {
     	/* Special treatment for associative operators with lots of children */
@@ -778,12 +778,12 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
     }
 
   | HEX_LITERAL
-    { Assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
+    { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
       std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
       expr = MK_CONST( BitVector(hexString, 16) ); }
 
   | BINARY_LITERAL
-    { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
+    { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
       std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
       expr = MK_CONST( BitVector(binString, 2) ); }
 
@@ -1055,7 +1055,9 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
         }
         t = EXPR_MANAGER->mkBitVectorType(numerals.front());
       } else {
-        Unhandled(name);
+        std::stringstream ss;
+        ss << "unknown indexed symbol `" << name << "'";
+        PARSER_STATE->parseError(ss.str());
       }
     }
   | LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index ca7697810..45caf94a8 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -88,7 +88,9 @@ void Smt2::addTheory(Theory theory) {
     break;
 
   default:
-    Unhandled(theory);
+    std::stringstream ss;
+    ss << "internal error: unsupported theory " << theory;
+    throw ParserException(ss.str());
   }
 }
 
diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index 8f43b0acf..dd90598bb 100644
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -34,7 +34,7 @@ namespace parser {
 Smt2Input::Smt2Input(AntlrInputStream& inputStream) :
   AntlrInput(inputStream, 2) {
   pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
-  AlwaysAssert( input != NULL );
+  assert( input != NULL );
 
   d_pSmt2Lexer = Smt2LexerNew(input);
   if( d_pSmt2Lexer == NULL ) {
@@ -44,7 +44,7 @@ Smt2Input::Smt2Input(AntlrInputStream& inputStream) :
   setAntlr3Lexer( d_pSmt2Lexer->pLexer );
 
   pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
-  AlwaysAssert( tokenStream != NULL );
+  assert( tokenStream != NULL );
 
   d_pSmt2Parser = Smt2ParserNew(tokenStream);
   if( d_pSmt2Parser == NULL ) {
@@ -61,12 +61,12 @@ Smt2Input::~Smt2Input() {
 }
 
 Command* Smt2Input::parseCommand()
-  throw (ParserException, TypeCheckingException, AssertionException) {
+  throw (ParserException, TypeCheckingException) {
   return d_pSmt2Parser->parseCommand(d_pSmt2Parser);
 }
 
 Expr Smt2Input::parseExpr()
-  throw (ParserException, TypeCheckingException, AssertionException) {
+  throw (ParserException, TypeCheckingException) {
   return d_pSmt2Parser->parseExpr(d_pSmt2Parser);
 }
 
diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h
index 05a62c30d..2e36b218e 100644
--- a/src/parser/smt2/smt2_input.h
+++ b/src/parser/smt2/smt2_input.h
@@ -78,7 +78,7 @@ protected:
    * @throws ParserException if an error is encountered during parsing.
    */
   Command* parseCommand()
-    throw(ParserException, TypeCheckingException, AssertionException);
+    throw(ParserException, TypeCheckingException);
 
   /**
    * Parse an expression from the input. Returns a null
@@ -87,7 +87,7 @@ protected:
    * @throws ParserException if an error is encountered during parsing.
    */
   Expr parseExpr()
-    throw(ParserException, TypeCheckingException, AssertionException);
+    throw(ParserException, TypeCheckingException);
 
 };/* class Smt2Input */
 
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());
   }
 }
 
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index 9d75a1d37..6d35cac61 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -24,6 +24,7 @@
 #include "parser/parser.h"
 #include "expr/command.h"
 #include <ext/hash_set>
+#include <cassert>
 
 namespace CVC4 {
 
@@ -52,9 +53,9 @@ class Tptp : public Parser {
 public:
   bool cnf; //in a cnf formula
 
-  void addFreeVar(Expr var){Assert(cnf); d_freeVar.push_back(var); };
+  void addFreeVar(Expr var){assert(cnf); d_freeVar.push_back(var); };
   std::vector< Expr > getFreeVar(){
-    Assert(cnf);
+    assert(cnf);
     std::vector< Expr > r;
     r.swap(d_freeVar);
     return r;
@@ -212,22 +213,19 @@ inline Command* Tptp::makeCommand(FormulaRole fr, Expr & expr){
   case FR_PLAIN:
     // it's a usual assert
     return new AssertCommand(expr);
-    break;
   case FR_CONJECTURE:
     // something to prove
     return new AssertCommand(getExprManager()->mkExpr(kind::NOT,expr));
-    break;
   case FR_UNKNOWN:
   case FR_FI_DOMAIN:
   case FR_FI_FUNCTORS:
   case FR_FI_PREDICATES:
   case FR_TYPE:
     return new EmptyCommand("Untreated role");
-    break;
-  default:
-    Unreachable("fr",fr);
-  };
-};
+  }
+  assert(false);// unreachable
+  return NULL;
+}
 
 namespace tptp {
 /**
diff --git a/src/parser/tptp/tptp_input.cpp b/src/parser/tptp/tptp_input.cpp
index 689f13a8b..8d41a5b68 100644
--- a/src/parser/tptp/tptp_input.cpp
+++ b/src/parser/tptp/tptp_input.cpp
@@ -34,7 +34,7 @@ namespace parser {
 TptpInput::TptpInput(AntlrInputStream& inputStream) :
   AntlrInput(inputStream, 1) {
   pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
-  AlwaysAssert( input != NULL );
+  assert( input != NULL );
 
   d_pTptpLexer = TptpLexerNew(input);
   if( d_pTptpLexer == NULL ) {
@@ -44,7 +44,7 @@ TptpInput::TptpInput(AntlrInputStream& inputStream) :
   setAntlr3Lexer( d_pTptpLexer->pLexer );
 
   pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
-  AlwaysAssert( tokenStream != NULL );
+  assert( tokenStream != NULL );
 
   d_pTptpParser = TptpParserNew(tokenStream);
   if( d_pTptpParser == NULL ) {
@@ -61,12 +61,12 @@ TptpInput::~TptpInput() {
 }
 
 Command* TptpInput::parseCommand()
-  throw (ParserException, TypeCheckingException, AssertionException) {
+  throw (ParserException, TypeCheckingException) {
   return d_pTptpParser->parseCommand(d_pTptpParser);
 }
 
 Expr TptpInput::parseExpr()
-  throw (ParserException, TypeCheckingException, AssertionException) {
+  throw (ParserException, TypeCheckingException) {
   return d_pTptpParser->parseExpr(d_pTptpParser);
 }
 
diff --git a/src/parser/tptp/tptp_input.h b/src/parser/tptp/tptp_input.h
index 7977117d0..32d3efad1 100644
--- a/src/parser/tptp/tptp_input.h
+++ b/src/parser/tptp/tptp_input.h
@@ -78,7 +78,7 @@ protected:
    * @throws ParserException if an error is encountered during parsing.
    */
   Command* parseCommand()
-    throw(ParserException, TypeCheckingException, AssertionException);
+    throw(ParserException, TypeCheckingException);
 
   /**
    * Parse an expression from the input. Returns a null
@@ -87,7 +87,7 @@ protected:
    * @throws ParserException if an error is encountered during parsing.
    */
   Expr parseExpr()
-    throw(ParserException, TypeCheckingException, AssertionException);
+    throw(ParserException, TypeCheckingException);
 
 };/* class TptpInput */