From c6fffe4fd328401f7f7e0757303e8dea5f6c14a4 Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Fri, 5 Mar 2021 16:17:15 -0800
Subject: 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.
---
 test/regress/regress0/bv/ackermann1.smt2         | 2 +-
 test/regress/regress0/bv/ackermann2.smt2         | 2 +-
 test/regress/regress0/bv/ackermann3.smt2         | 2 +-
 test/regress/regress0/bv/ackermann4.smt2         | 2 +-
 test/regress/regress0/bv/bv-options4.smt2        | 2 +-
 test/regress/regress0/bv/core/constant_core.smt2 | 2 +-
 test/regress/regress0/bv/inequality00.smt2       | 2 +-
 test/regress/regress0/bv/inequality01.smt2       | 2 +-
 test/regress/regress0/bv/inequality02.smt2       | 2 +-
 test/regress/regress0/bv/inequality03.smt2       | 2 +-
 test/regress/regress0/bv/inequality04.smt2       | 2 +-
 test/regress/regress0/bv/inequality05.smt2       | 2 +-
 12 files changed, 12 insertions(+), 12 deletions(-)

(limited to 'test/regress/regress0/bv')

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))
-- 
cgit v1.2.3