* Rename SMT parts (printer, parser) to SMT1

* Change --lang smt to mean SMT-LIBv2
* --lang smt1 now means SMT-LIBv1

* SMT-LIBv2 parser now gives helpful error if input looks like v1
* SMT-LIBv1 parser now gives helpful error if input looks like v2
* CVC presentation language parser now gives helpful error if input
  looks like either SMT-LIB v1 or v2

* Other associated changes

(this commit was certified error- and warning-free by the test-and-commit script.)

2 files changed, 8 insertions, 8 deletions

diff --git a/test/regress/run_regression b/test/regress/run_regression
index 5ed43d1a0..97941653c 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -57,7 +57,7 @@ function gettemp {
 tmpbenchmark=
 if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
   proof_command=PROOFS-NOT-SUPPORTED-IN-SMTLIB-V1
-  lang=smt
+  lang=smt1
   if test -e "$benchmark.expect"; then
     expected_proof=`grep -q '^% PROOF' "$benchmark.expect" && echo yes`
     expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'`
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 01879ec49..bfa2ddc44 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -282,11 +282,11 @@ public:
   }
 };/* class Cvc4ParserTest */
 
-class SmtParserTest : public CxxTest::TestSuite, public ParserBlack {
+class Smt1ParserTest : public CxxTest::TestSuite, public ParserBlack {
   typedef ParserBlack super;
 
 public:
-  SmtParserTest() : ParserBlack(LANG_SMTLIB) { }
+  Smt1ParserTest() : ParserBlack(LANG_SMTLIB_V1) { }
 
   void setUp() {
     super::setUp();
@@ -296,7 +296,7 @@ public:
     super::tearDown();
   }
 
-  void testGoodSmtInputs() {
+  void testGoodSmt1Inputs() {
     tryGoodInput(""); // empty string is OK
     tryGoodInput("(benchmark foo :assumption true)");
     tryGoodInput("(benchmark bar :formula true)");
@@ -309,7 +309,7 @@ public:
     tryGoodInput("; a comment\n(benchmark foo ; hello\n  :formula true; goodbye\n)");
   }
 
-  void testBadSmtInputs() {
+  void testBadSmt1Inputs() {
 // competition builds don't do any checking
 #ifndef CVC4_COMPETITION_MODE
     tryBadInput("(benchmark foo)"); // empty benchmark is not OK
@@ -320,7 +320,7 @@ public:
 #endif /* ! CVC4_COMPETITION_MODE */
   }
 
-  void testGoodSmtExprs() {
+  void testGoodSmt1Exprs() {
     tryGoodExpr("(and a b)");
     tryGoodExpr("(or (and a b) c)");
     tryGoodExpr("(implies (and (implies a b) a) b)");
@@ -333,7 +333,7 @@ public:
     tryGoodExpr("1.5");
   }
 
-  void testBadSmtExprs() {
+  void testBadSmt1Exprs() {
 // competition builds don't do any checking
 #ifndef CVC4_COMPETITION_MODE
     tryBadExpr("(and)"); // wrong arity
@@ -349,7 +349,7 @@ public:
     tryBadExpr("1."); // rational constants must have fractional suffix
 #endif /* ! CVC4_COMPETITION_MODE */
   }
-};/* class SmtParserTest */
+};/* class Smt1ParserTest */
 
 class Smt2ParserTest : public CxxTest::TestSuite, public ParserBlack {
   typedef ParserBlack super;