Make user's SMT2 version override file version (#2004)

5 files changed, 22 insertions, 3 deletions

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 09f7a5696..3def5696b 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -171,6 +171,7 @@ public:
   {
     return language::isInputLang_smt2_6(getLanguage(), exact);
   }
+
   bool sygus() const { return getLanguage() == language::input::LANG_SYGUS; }
 
   void setInfo(const std::string& flag, const SExpr& sexpr);
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6ecf00ccd..097b41d93 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2363,7 +2363,9 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
   } else if(key == "name") {
     d_filename = value.getValue();
     return;
-  } else if(key == "smt-lib-version") {
+  }
+  else if (key == "smt-lib-version" && !options::inputLanguage.wasSetByUser())
+  {
     language::input::Language ilang = language::input::LANG_AUTO;
     if( (value.isInteger() && value.getIntegerValue() == Integer(2)) ||
         (value.isRational() && value.getRationalValue() == Rational(2)) ||
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index bd5002921..36f0d945e 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -162,11 +162,11 @@ REG0_TESTS = \
 	regress0/bv/bug734.smt2 \
 	regress0/bv/bv-int-collapse1.smt2 \
 	regress0/bv/bv-int-collapse2.smt2 \
-	regress0/bv/bv-to-bool.smt \
 	regress0/bv/bv-options1.smt2 \
 	regress0/bv/bv-options2.smt2 \
 	regress0/bv/bv-options3.smt2 \
 	regress0/bv/bv-options4.smt2 \
+	regress0/bv/bv-to-bool.smt \
 	regress0/bv/bv2nat-ground-c.smt2 \
 	regress0/bv/bv2nat-simp-range.smt2 \
 	regress0/bv/bvmul-pow2-only.smt2 \
@@ -475,6 +475,8 @@ REG0_TESTS = \
 	regress0/ite4.smt2 \
 	regress0/ite_real_int_type.smt \
 	regress0/ite_real_valid.smt \
+	regress0/lang_opts_2_5.smt2 \
+	regress0/lang_opts_2_6_1.smt2 \
 	regress0/lemmas/clocksynchro_5clocks.main_invar.base.model.smt \
 	regress0/lemmas/fs_not_sc_seen.induction.smt \
 	regress0/lemmas/mode_cntrl.induction.smt \
@@ -595,9 +597,9 @@ REG0_TESTS = \
 	regress0/quantifiers/ex3.smt2 \
 	regress0/quantifiers/ex6.smt2 \
 	regress0/quantifiers/floor.smt2 \
-	regress0/quantifiers/issue1805.smt2 \
 	regress0/quantifiers/is-even-pred.smt2 \
 	regress0/quantifiers/is-int.smt2 \
+	regress0/quantifiers/issue1805.smt2 \
 	regress0/quantifiers/lra-triv-gn.smt2 \
 	regress0/quantifiers/macros-int-real.smt2 \
 	regress0/quantifiers/macros-real-arg.smt2 \
diff --git a/test/regress/regress0/lang_opts_2_5.smt2 b/test/regress/regress0/lang_opts_2_5.smt2
new file mode 100644
index 000000000..5a56960f0
--- /dev/null
+++ b/test/regress/regress0/lang_opts_2_5.smt2
@@ -0,0 +1,7 @@
+; Check that the language set in the command line options has higher priority
+; than the language specified in the input file.
+;
+; COMMAND-LINE: --lang=smt2.5
+; EXPECT: "LANG_SMTLIB_V2_5"
+(set-info :smt-lib-version 2.6)
+(get-option :input-language)
diff --git a/test/regress/regress0/lang_opts_2_6_1.smt2 b/test/regress/regress0/lang_opts_2_6_1.smt2
new file mode 100644
index 000000000..bb005d527
--- /dev/null
+++ b/test/regress/regress0/lang_opts_2_6_1.smt2
@@ -0,0 +1,7 @@
+; Check that the language set in the command line options has higher priority
+; than the language specified in the input file.
+;
+; COMMAND-LINE: --lang=smt2.6.1
+; EXPECT: "LANG_SMTLIB_V2_6_1"
+(set-info :smt-lib-version 2.6)
+(get-option :input-language)