true and false are only defined if the core theory is loaded in SMT v2 strict mode

1 files changed, 8 insertions, 0 deletions

diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index bcefe166b..6d7a04800 100644
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -20,6 +20,7 @@
 #include "parser/input.h"
 #include "parser/parser.h"
 #include "parser/parser_exception.h"
+#include "parser/smt2/smt2.h"
 #include "parser/smt2/generated/Smt2Lexer.h"
 #include "parser/smt2/generated/Smt2Parser.h"
 
@@ -64,5 +65,12 @@ Expr Smt2Input::parseExpr() throw (ParserException) {
   return d_pSmt2Parser->parseExpr(d_pSmt2Parser);
 }
 
+void Smt2Input::setParser(Parser& parser) {
+  super::setParser(parser);
+  if( !parser.strictModeEnabled() ) {
+    Smt2::addTheory(parser,Smt2::THEORY_CORE);
+  }
+}
+
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */