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.

12 files changed, 12 insertions, 12 deletions

diff --git a/test/regress/regress0/bv/ackermann1.smt2 b/test/regress/regress0/bv/ackermann1.smt2
index bdf74ce49..fa1963322 100644
--- a/test/regress/regress0/bv/ackermann1.smt2
+++ b/test/regress/regress0/bv/ackermann1.smt2
@@ -2,7 +2,7 @@
 ; COMMAND-LINE: --bitblast=eager --bv-solver=simple --no-check-models  --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_UFBV)
-(set-info :smt-lib-version 2.0)
+(set-info :smt-lib-version 2.6)
 (set-info :category "crafted")
 (declare-fun v0 () (_ BitVec 4))
 (declare-fun f ((_ BitVec 4)) (_ BitVec 4))
diff --git a/test/regress/regress0/bv/ackermann2.smt2 b/test/regress/regress0/bv/ackermann2.smt2
index 518faf597..80b8126a0 100644
--- a/test/regress/regress0/bv/ackermann2.smt2
+++ b/test/regress/regress0/bv/ackermann2.smt2
@@ -4,7 +4,7 @@
 ; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_UFBV)
-(set-info :smt-lib-version 2.0)
+(set-info :smt-lib-version 2.6)
 (set-info :category "crafted")
 (set-info :status unsat)
 (declare-fun v0 () (_ BitVec 4))
diff --git a/test/regress/regress0/bv/ackermann3.smt2 b/test/regress/regress0/bv/ackermann3.smt2
index ec3efeedd..9b44b8d63 100644
--- a/test/regress/regress0/bv/ackermann3.smt2
+++ b/test/regress/regress0/bv/ackermann3.smt2
@@ -1,7 +1,7 @@
 ; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_ABV)
-(set-info :smt-lib-version 2.0)
+(set-info :smt-lib-version 2.6)
 (set-info :category "crafted")
 (set-info :status unsat)
 
diff --git a/test/regress/regress0/bv/ackermann4.smt2 b/test/regress/regress0/bv/ackermann4.smt2
index 05ffef452..69bf76937 100644
--- a/test/regress/regress0/bv/ackermann4.smt2
+++ b/test/regress/regress0/bv/ackermann4.smt2
@@ -1,7 +1,7 @@
 ; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_UFBV)
-(set-info :smt-lib-version 2.0)
+(set-info :smt-lib-version 2.6)
 (set-info :category "crafted")
 (declare-fun v0 () (_ BitVec 4))
 (declare-fun f ((_ BitVec 4)) (_ BitVec 4))
diff --git a/test/regress/regress0/bv/bv-options4.smt2 b/test/regress/regress0/bv/bv-options4.smt2
index b7a78e3b5..f804f1133 100644
--- a/test/regress/regress0/bv/bv-options4.smt2
+++ b/test/regress/regress0/bv/bv-options4.smt2
@@ -2,7 +2,7 @@
 ; EXPECT: unsat
 ; EXIT: 0
 (set-logic QF_BV)
-(set-info :smt-lib-version 2.0)
+(set-info :smt-lib-version 2.6)
 (set-info :category "crafted")
 (declare-fun v0 () (_ BitVec 16))
 (declare-fun v1 () (_ BitVec 16))
diff --git a/test/regress/regress0/bv/core/constant_core.smt2 b/test/regress/regress0/bv/core/constant_core.smt2
index 1e2bcde68..a353a5c6f 100644
--- a/test/regress/regress0/bv/core/constant_core.smt2
+++ b/test/regress/regress0/bv/core/constant_core.smt2
@@ -1,5 +1,5 @@
 (set-logic QF_BV)
-(set-info :smt-lib-version 2.0)
+(set-info :smt-lib-version 2.6)
 (set-info :category "crafted")
 (set-info :status unsat)
 (declare-fun x () (_ BitVec 3))
diff --git a/test/regress/regress0/bv/inequality00.smt2 b/test/regress/regress0/bv/inequality00.smt2
index dc6285d52..c95b7caa6 100644
--- a/test/regress/regress0/bv/inequality00.smt2
+++ b/test/regress/regress0/bv/inequality00.smt2
@@ -1,5 +1,5 @@
 (set-logic QF_BV)
-(set-info :smt-lib-version 2.0)
+(set-info :smt-lib-version 2.6)
 (set-info :category "crafted")
 (set-info :status unsat)
 (declare-fun v0 () (_ BitVec 16))
diff --git a/test/regress/regress0/bv/inequality01.smt2 b/test/regress/regress0/bv/inequality01.smt2
index 73a2515df..f094d0d11 100644
--- a/test/regress/regress0/bv/inequality01.smt2
+++ b/test/regress/regress0/bv/inequality01.smt2
@@ -1,5 +1,5 @@
 (set-logic QF_BV)
-(set-info :smt-lib-version 2.0)
+(set-info :smt-lib-version 2.6)
 (set-info :category "crafted")
 (set-info :status sat)
 (declare-fun v0 () (_ BitVec 16))
diff --git a/test/regress/regress0/bv/inequality02.smt2 b/test/regress/regress0/bv/inequality02.smt2
index 05f11311f..75ecc47f4 100644
--- a/test/regress/regress0/bv/inequality02.smt2
+++ b/test/regress/regress0/bv/inequality02.smt2
@@ -1,5 +1,5 @@
 (set-logic QF_BV)
-(set-info :smt-lib-version 2.0)
+(set-info :smt-lib-version 2.6)
 (set-info :category "crafted")
 (set-info :status unsat)
 (declare-fun v0 () (_ BitVec 16))
diff --git a/test/regress/regress0/bv/inequality03.smt2 b/test/regress/regress0/bv/inequality03.smt2
index a47551d14..d69b978f7 100644
--- a/test/regress/regress0/bv/inequality03.smt2
+++ b/test/regress/regress0/bv/inequality03.smt2
@@ -1,5 +1,5 @@
 (set-logic QF_BV)
-(set-info :smt-lib-version 2.0)
+(set-info :smt-lib-version 2.6)
 (set-info :category "crafted")
 (set-info :status unsat)
 (declare-fun v0 () (_ BitVec 16))
diff --git a/test/regress/regress0/bv/inequality04.smt2 b/test/regress/regress0/bv/inequality04.smt2
index 35607eaef..dc02322b1 100644
--- a/test/regress/regress0/bv/inequality04.smt2
+++ b/test/regress/regress0/bv/inequality04.smt2
@@ -1,5 +1,5 @@
 (set-logic QF_BV)
-(set-info :smt-lib-version 2.0)
+(set-info :smt-lib-version 2.6)
 (set-info :category "crafted")
 (set-info :status unsat)
 (declare-fun v0 () (_ BitVec 16))
diff --git a/test/regress/regress0/bv/inequality05.smt2 b/test/regress/regress0/bv/inequality05.smt2
index d8cf9cf99..df9f5a23a 100644
--- a/test/regress/regress0/bv/inequality05.smt2
+++ b/test/regress/regress0/bv/inequality05.smt2
@@ -1,5 +1,5 @@
 (set-logic QF_BV)
-(set-info :smt-lib-version 2.0)
+(set-info :smt-lib-version 2.6)
 (set-info :category "crafted")
 (set-info :status sat)
 (declare-fun v0 () (_ BitVec 16))