3 files changed, 15 insertions, 11 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index d788a2c3f..a393bc85f 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -209,14 +209,6 @@ void Parser::checkArity(Kind kind, unsigned int numArgs)
   }
 }
 
-void Parser::enableChecks() {
-  d_checksEnabled = true;
-}
-
-void Parser::disableChecks() {
-  d_checksEnabled = false;
-}
-
 Command* Parser::nextCommand() throw(ParserException) {
   Debug("parser") << "nextCommand()" << std::endl;
   Command* cmd = NULL;
diff --git a/src/parser/parser.h b/src/parser/parser.h
index f56ec03ac..25d7f2cd1 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -113,6 +113,8 @@ class CVC4_PUBLIC Parser {
   /** Are semantic checks enabled during parsing? */
   bool d_checksEnabled;
 
+  /** Are we parsing in strict mode? */
+  bool d_strictMode;
 
   /** Lookup a symbol in the given namespace. */
   Expr getSymbol(const std::string& var_name, SymbolType type);
@@ -158,10 +160,18 @@ public:
   }
 
   /** Enable semantic checks during parsing. */
-  void enableChecks();
+  void enableChecks() { d_checksEnabled = true; }
 
   /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */
-  void disableChecks();
+  void disableChecks() { d_checksEnabled = false; }
+
+  /** Enable strict parsing, according to the language standards. */
+  void enableStrictMode() { d_strictMode = true; }
+
+  /** Disable strict parsing. Allows certain syntactic infelicities to pass without comment. */
+  void disableStrictMode() { d_strictMode = false; }
+
+  bool strictModeEnabled() { return d_strictMode; }
 
   /** Get the name of the input file. */
 /*
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index fd5e334ed..bcab39183 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -208,7 +208,9 @@ term[CVC4::Expr& expr]
 } 
   : /* a built-in operator application */
     LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK 
-    { if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) {
+    { if( !PARSER_STATE->strictModeEnabled() && 
+          (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] );