Disallow overflow in bitvector literals (parser only)

* For example, (_ bv5 1) is now an error instead of being silently truncated.
* Probably inappropriate for 1.0.x because it changes exception specifications.

2 files changed, 4 insertions, 8 deletions

diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp
index 52fadae66..8328306be 100644
--- a/src/parser/cvc/cvc_input.cpp
+++ b/src/parser/cvc/cvc_input.cpp
@@ -56,13 +56,11 @@ CvcInput::~CvcInput() {
   d_pCvcParser->free(d_pCvcParser);
 }
 
-Command* CvcInput::parseCommand()
-  throw (ParserException, TypeCheckingException) {
+Command* CvcInput::parseCommand() {
   return d_pCvcParser->parseCommand(d_pCvcParser);
 }
 
-Expr CvcInput::parseExpr()
-  throw (ParserException, TypeCheckingException) {
+Expr CvcInput::parseExpr() {
   return d_pCvcParser->parseExpr(d_pCvcParser);
 }
 
diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h
index 398ac4bd0..973e1c173 100644
--- a/src/parser/cvc/cvc_input.h
+++ b/src/parser/cvc/cvc_input.h
@@ -63,16 +63,14 @@ protected:
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Command* parseCommand() 
-    throw(ParserException, TypeCheckingException);
+  Command* parseCommand();
 
   /** Parse an expression from the input. Returns a null <code>Expr</code>
    * if there is no expression there to parse.
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Expr parseExpr() 
-    throw(ParserException, TypeCheckingException);
+  Expr parseExpr();
 
 private: