4 files changed, 17 insertions, 12 deletions
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 96ac46bf1..86682f9a9 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -474,8 +474,8 @@ identifier[std::string& id,
   : IDENTIFIER
     { id = AntlrInput::tokenText($IDENTIFIER);
       Debug("parser") << "identifier: " << id
-                      << " check? " << toString(check)
-                      << " type? " << toString(type) << std::endl;
+                      << " check? " << check
+                      << " type? " << type << std::endl;
       PARSER_STATE->checkDeclaration(id, check, type); }
   ;
 
@@ -489,7 +489,7 @@ let_identifier[std::string& id,
   : LET_IDENTIFIER
     { id = AntlrInput::tokenText($LET_IDENTIFIER);
       Debug("parser") << "let_identifier: " << id
-                      << " check? " << toString(check) << std::endl;
+                      << " check? " << check << std::endl;
       PARSER_STATE->checkDeclaration(id, check, SYM_VARIABLE); }
   ;
 
@@ -503,7 +503,7 @@ flet_identifier[std::string& id,
   : FLET_IDENTIFIER
     { id = AntlrInput::tokenText($FLET_IDENTIFIER);
       Debug("parser") << "flet_identifier: " << id
-                      << " check? " << toString(check) << std::endl;
+                      << " check? " << check << std::endl;
       PARSER_STATE->checkDeclaration(id, check); }
   ;
 
diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index bfac4f300..a8dabeffe 100644
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters, dejan
+ ** Minor contributors (to current version): dejan, mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -47,8 +47,8 @@ Smt::Logic Smt::toLogic(const std::string& name) {
   return logicMap[name];
 }
 
-Smt::Smt(ExprManager* exprManager, Input* input, bool strictMode) :
-  Parser(exprManager,input,strictMode),
+Smt::Smt(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
+  Parser(exprManager,input,strictMode,parseOnly),
   d_logicSet(false) {
 
   // Boolean symbols are always defined
diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h
index 388b4cd6d..98ebf6410 100644
--- a/src/parser/smt/smt.h
+++ b/src/parser/smt/smt.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -78,7 +78,7 @@ private:
   Logic d_logic;
 
 protected:
-  Smt(ExprManager* exprManager, Input* input, bool strictMode = false);
+  Smt(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
 
 public:
   /**
diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h
index c5b147b71..0ab382c73 100644
--- a/src/parser/smt/smt_input.h
+++ b/src/parser/smt/smt_input.h
@@ -55,6 +55,11 @@ public:
   /** Destructor. Frees the lexer and the parser. */
   ~SmtInput();
 
+  /** Get the language that this Input is reading. */
+  InputLanguage getLanguage() const throw() {
+    return language::input::LANG_SMTLIB;
+  }
+
 protected:
 
   /**
@@ -63,7 +68,7 @@ protected:
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Command* parseCommand() 
+  Command* parseCommand()
     throw(ParserException, TypeCheckingException, AssertionException);
 
   /**
@@ -72,7 +77,7 @@ protected:
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Expr parseExpr() 
+  Expr parseExpr()
     throw(ParserException, TypeCheckingException, AssertionException);
 
 private: