4 files changed, 15 insertions, 11 deletions
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 */