3 files changed, 36 insertions, 15 deletions
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index f52467ad9..38fe1bce8 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -29,6 +29,7 @@
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "util/Assert.h"
+#include "util/bitvector.h"
 #include "util/integer.h"
 #include "util/rational.h"
 
@@ -148,8 +149,6 @@ public:
   static Integer tokenToInteger( pANTLR3_COMMON_TOKEN token );
   /** Retrieve a Rational from the text of a token */
   static Rational tokenToRational(pANTLR3_COMMON_TOKEN token);
-  /** Retrive a Bitvector from the text of a token */
-//  static Bitvector tokenToBitvector(pANTLR3_COMMON_TOKEN token, int base);
 
 protected:
   /** Create an input. This input takes ownership of the given input stream,
@@ -201,8 +200,7 @@ inline unsigned AntlrInput::tokenToUnsigned(pANTLR3_COMMON_TOKEN token) {
 }
 
 inline Integer AntlrInput::tokenToInteger(pANTLR3_COMMON_TOKEN token) {
-  Integer i( tokenText(token) );
-  return i;
+  return Integer( tokenText(token) );
 }
 
 inline Rational AntlrInput::tokenToRational(pANTLR3_COMMON_TOKEN token) {
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 01cc99c3d..d788a2c3f 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -241,8 +241,9 @@ Expr Parser::nextExpression() throw(ParserException) {
   if(!done()) {
     try {
       result = d_input->parseExpr();
-      if(result.isNull())
+      if(result.isNull()) {
         setDone();
+      }
     } catch(ParserException& e) {
       setDone();
       throw;
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 19997cdd0..4f65fa5e7 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -259,6 +259,14 @@ term[CVC4::Expr& expr]
   | RATIONAL
     { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string
       expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL) ); }
+  | HEX_LITERAL
+    { std::string hexString = AntlrInput::tokenText($HEX_LITERAL);
+      AlwaysAssert( hexString.find("#x") == 0 );
+      expr = MK_CONST( BitVector(hexString.erase(0,2), 16) ); }
+  | BINARY_LITERAL
+    { std::string binString = AntlrInput::tokenText($BINARY_LITERAL);
+      AlwaysAssert( binString.find("#b") == 0 );
+      expr = MK_CONST( BitVector(binString.erase(0,2), 2) ); }
     // NOTE: Theory constants go here
   ;
 
@@ -352,15 +360,6 @@ sortSymbol[CVC4::Type& t]
   ;
 
 /**
- * Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'.
- */
-benchmarkStatus[ CVC4::BenchmarkStatus& status ]
-  : SAT_TOK       { $status = SMT_SATISFIABLE;    }
-  | UNSAT_TOK     { $status = SMT_UNSATISFIABLE;  }
-  | UNKNOWN_TOK   { $status = SMT_UNKNOWN;        }
-  ;
-
-/**
  * Matches an symbol and sets the string reference parameter id.
  * @param id string to hold the symbol
  * @param check what kinds of check to do on the symbol
@@ -459,17 +458,38 @@ WHITESPACE
   ;
 
 /**
- * Matches a numeral from the input (non-empty sequence of digits).
+ * Matches an integer constant from the input (non-empty sequence of digits).
+ * This is a bit looser than what the standard allows, because it accepts 
+ * leading zeroes. 
  */
 NUMERAL
   : DIGIT+
   ;
 
+/**
+  * Matches a rational constant from the input. This is a bit looser
+  * than what the standard allows, because it accepts leading zeroes. 
+  */
 RATIONAL
   : DIGIT+ '.' DIGIT+
   ;
 
 /**
+ * Matches a hexadecimal constant.
+ */
+ HEX_LITERAL
+  : '#x' HEX_DIGIT+
+  ;
+
+/**
+ * Matches a binary constant.
+ */
+ BINARY_LITERAL
+  : '#b' ('0' | '1')+
+  ;
+
+
+/**
  * Matches a double quoted string literal. Escaping is supported, and escape
  * character '\' has to be escaped.
  */
@@ -499,6 +519,8 @@ ALPHA
  */
 fragment DIGIT : '0'..'9';
 
+fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
+
 /** Matches the characters that may appear in a "symbol" (i.e., an identifier) 
  */
 fragment SYMBOL_CHAR