summaryrefslogtreecommitdiff
path: root/test/regress/regress0/quantifiers
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2021-03-05 16:17:15 -0800
committerGitHub <noreply@github.com>2021-03-06 00:17:15 +0000
commitc6fffe4fd328401f7f7e0757303e8dea5f6c14a4 (patch)
tree84bbb3f44fa7ffbeba0c0baf9b7b22f036d2e9f4 /test/regress/regress0/quantifiers
parent555e4b0b6b10e9170676c0a3ef9b778322f3327f (diff)
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.
Diffstat (limited to 'test/regress/regress0/quantifiers')
-rw-r--r--test/regress/regress0/quantifiers/bug290.smt22
-rw-r--r--test/regress/regress0/quantifiers/bug291.smt22
-rw-r--r--test/regress/regress0/quantifiers/ex3.smt22
-rw-r--r--test/regress/regress0/quantifiers/ex6.smt22
4 files changed, 4 insertions, 4 deletions
diff --git a/test/regress/regress0/quantifiers/bug290.smt2 b/test/regress/regress0/quantifiers/bug290.smt2
index 650d6aab0..fb2955eb0 100644
--- a/test/regress/regress0/quantifiers/bug290.smt2
+++ b/test/regress/regress0/quantifiers/bug290.smt2
@@ -1,6 +1,6 @@
(set-logic AUFLIA)
(set-info :source | Simple list theorem |)
-(set-info :smt-lib-version 2.0)
+(set-info :smt-lib-version 2.6)
(set-info :category "crafted")
(set-info :status unsat)
(declare-sort List 0)
diff --git a/test/regress/regress0/quantifiers/bug291.smt2 b/test/regress/regress0/quantifiers/bug291.smt2
index 959d83c7f..c8e3111c8 100644
--- a/test/regress/regress0/quantifiers/bug291.smt2
+++ b/test/regress/regress0/quantifiers/bug291.smt2
@@ -5,7 +5,7 @@
Boogie/Spec# benchmarks.
This benchmark was translated by Michal Moskal.
|)
-(set-info :smt-lib-version 2.0)
+(set-info :smt-lib-version 2.6)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun select2 (Int) Int)
diff --git a/test/regress/regress0/quantifiers/ex3.smt2 b/test/regress/regress0/quantifiers/ex3.smt2
index fd887b4bc..c08908e30 100644
--- a/test/regress/regress0/quantifiers/ex3.smt2
+++ b/test/regress/regress0/quantifiers/ex3.smt2
@@ -1,5 +1,5 @@
(set-logic AUFLIRA)
-(set-info :smt-lib-version 2.0)
+(set-info :smt-lib-version 2.6)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort U 0)
diff --git a/test/regress/regress0/quantifiers/ex6.smt2 b/test/regress/regress0/quantifiers/ex6.smt2
index 7285e1c4f..294869277 100644
--- a/test/regress/regress0/quantifiers/ex6.smt2
+++ b/test/regress/regress0/quantifiers/ex6.smt2
@@ -1,5 +1,5 @@
(set-logic AUFLIRA)
-(set-info :smt-lib-version 2.0)
+(set-info :smt-lib-version 2.6)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort U 0)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback