Remove SMT-LIB 2.5 and 2.0 support. (#6068)

This commit removes parser and printer support for old SMT-LIB standards and also converts all regression tests to 2.6.

7 files changed, 7 insertions, 7 deletions

diff --git a/test/regress/regress1/arith/bug716.0.smt2 b/test/regress/regress1/arith/bug716.0.smt2
index dd2501bbb..9e05e8b3d 100644
--- a/test/regress/regress1/arith/bug716.0.smt2
+++ b/test/regress/regress1/arith/bug716.0.smt2
@@ -7,7 +7,7 @@
 (set-logic AUFBVDTLIRA)
 ;; produced by cvc4_15.drv ;;
 (set-info :source |VC generated by SPARK 2014|)
-(set-info :smt-lib-version 2.0)
+(set-info :smt-lib-version 2.6)
 (set-info :category industrial)
 (set-info :status unknown)
 ;;; generated by SMT-LIB2 driver
diff --git a/test/regress/regress1/arith/div.03.smt2 b/test/regress/regress1/arith/div.03.smt2
index 8beef7a69..51568b706 100644
--- a/test/regress/regress1/arith/div.03.smt2
+++ b/test/regress/regress1/arith/div.03.smt2
@@ -1,6 +1,6 @@
 ; EXPECT: unsat
 (set-logic QF_NIA)
-(set-info :smt-lib-version 2.0)
+(set-info :smt-lib-version 2.6)
 (set-info :status unsat)
 (declare-fun x () Int)
 (declare-fun n () Int)
diff --git a/test/regress/regress1/arith/div.06.smt2 b/test/regress/regress1/arith/div.06.smt2
index 45d687cab..b6a72d36f 100644
--- a/test/regress/regress1/arith/div.06.smt2
+++ b/test/regress/regress1/arith/div.06.smt2
@@ -1,7 +1,7 @@
 ; COMMAND-LINE: -q
 ; EXPECT: sat
 (set-logic QF_NRA)
-(set-info :smt-lib-version 2.0)
+(set-info :smt-lib-version 2.6)
 (set-info :status sat)
 (declare-fun x () Real)
 (declare-fun y () Real)
diff --git a/test/regress/regress1/arith/div.08.smt2 b/test/regress/regress1/arith/div.08.smt2
index 0b0d73ac1..d43110947 100644
--- a/test/regress/regress1/arith/div.08.smt2
+++ b/test/regress/regress1/arith/div.08.smt2
@@ -1,5 +1,5 @@
 (set-logic QF_NIA)
-(set-info :smt-lib-version 2.0)
+(set-info :smt-lib-version 2.6)
 (set-info :status unsat)
 (declare-fun n () Int)
 
diff --git a/test/regress/regress1/arith/mod.02.smt2 b/test/regress/regress1/arith/mod.02.smt2
index ee4333ea5..770de4c45 100644
--- a/test/regress/regress1/arith/mod.02.smt2
+++ b/test/regress/regress1/arith/mod.02.smt2
@@ -1,6 +1,6 @@
 ; EXPECT: unsat
 (set-logic QF_NIA)
-(set-info :smt-lib-version 2.0)
+(set-info :smt-lib-version 2.6)
 (set-info :status unsat)
 (declare-fun n () Int)
 
diff --git a/test/regress/regress1/arith/mod.03.smt2 b/test/regress/regress1/arith/mod.03.smt2
index 583c72a93..58dbd2319 100644
--- a/test/regress/regress1/arith/mod.03.smt2
+++ b/test/regress/regress1/arith/mod.03.smt2
@@ -1,7 +1,7 @@
 ; COMMAND-LINE: -q
 ; EXPECT: sat
 (set-logic QF_NIA)
-(set-info :smt-lib-version 2.0)
+(set-info :smt-lib-version 2.6)
 (set-info :status sat)
 (declare-fun n () Int)
 (declare-fun x () Int)
diff --git a/test/regress/regress1/arith/problem__003.smt2 b/test/regress/regress1/arith/problem__003.smt2
index 7af727e2a..fe177362c 100644
--- a/test/regress/regress1/arith/problem__003.smt2
+++ b/test/regress/regress1/arith/problem__003.smt2
@@ -3,7 +3,7 @@
 Alberto Griggio
 
 |)
-(set-info :smt-lib-version 2.0)
+(set-info :smt-lib-version 2.6)
 (set-info :category "random")
 (set-info :status sat)
 (declare-fun x0 () Int)