diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-03-05 16:17:15 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-06 00:17:15 +0000 |
commit | c6fffe4fd328401f7f7e0757303e8dea5f6c14a4 (patch) | |
tree | 84bbb3f44fa7ffbeba0c0baf9b7b22f036d2e9f4 /test/regress/regress0 | |
parent | 555e4b0b6b10e9170676c0a3ef9b778322f3327f (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')
108 files changed, 113 insertions, 146 deletions
diff --git a/test/regress/regress0/arith/bug569.smt2 b/test/regress/regress0/arith/bug569.smt2 index e1ca49ac5..c9a84d1ec 100644 --- a/test/regress/regress0/arith/bug569.smt2 +++ b/test/regress/regress0/arith/bug569.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_AUFLIRA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status unsat) (declare-fun v1 () Int) diff --git a/test/regress/regress0/arith/div.01.smt2 b/test/regress/regress0/arith/div.01.smt2 index d7d587021..7330790f8 100644 --- a/test/regress/regress0/arith/div.01.smt2 +++ b/test/regress/regress0/arith/div.01.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/regress0/arith/div.02.smt2 b/test/regress/regress0/arith/div.02.smt2 index 37dfcbbc1..4706c2a55 100644 --- a/test/regress/regress0/arith/div.02.smt2 +++ b/test/regress/regress0/arith/div.02.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) diff --git a/test/regress/regress0/arith/div.04.smt2 b/test/regress/regress0/arith/div.04.smt2 index c30b1cd2f..19124d3fc 100644 --- a/test/regress/regress0/arith/div.04.smt2 +++ b/test/regress/regress0/arith/div.04.smt2 @@ -1,5 +1,5 @@ (set-logic QF_NRA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :status unsat) (declare-fun x () Real) (declare-fun y () Real) diff --git a/test/regress/regress0/arith/div.05.smt2 b/test/regress/regress0/arith/div.05.smt2 index fd3e4ae48..99e6b04d5 100644 --- a/test/regress/regress0/arith/div.05.smt2 +++ b/test/regress/regress0/arith/div.05.smt2 @@ -1,6 +1,6 @@ ; 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/regress0/arith/div.07.smt2 b/test/regress/regress0/arith/div.07.smt2 index 4c45b32c8..5f1fcb060 100644 --- a/test/regress/regress0/arith/div.07.smt2 +++ b/test/regress/regress0/arith/div.07.smt2 @@ -1,5 +1,5 @@ (set-logic QF_NRA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :status unsat) (declare-fun x () Real) (declare-fun y () Real) diff --git a/test/regress/regress0/arith/integers/ackermann4.smt2 b/test/regress/regress0/arith/integers/ackermann4.smt2 index 34aa56480..bf55b41c2 100644 --- a/test/regress/regress0/arith/integers/ackermann4.smt2 +++ b/test/regress/regress0/arith/integers/ackermann4.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_ALIA) -(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/arith/integers/ackermann5.smt2 b/test/regress/regress0/arith/integers/ackermann5.smt2 index debd29344..8d6f124cd 100644 --- a/test/regress/regress0/arith/integers/ackermann5.smt2 +++ b/test/regress/regress0/arith/integers/ackermann5.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --ackermann --no-check-models ; EXPECT: sat (set-logic QF_UFLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (declare-fun v0 () Int) (declare-fun f (Int) Int) diff --git a/test/regress/regress0/arith/integers/ackermann6.smt2 b/test/regress/regress0/arith/integers/ackermann6.smt2 index 78f5a3658..96bf54703 100644 --- a/test/regress/regress0/arith/integers/ackermann6.smt2 +++ b/test/regress/regress0/arith/integers/ackermann6.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_UFLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (declare-fun v0 () Int) (declare-fun f (Int) Int) diff --git a/test/regress/regress0/arith/mod.01.smt2 b/test/regress/regress0/arith/mod.01.smt2 index 3a6d9a3d3..c83954628 100644 --- a/test/regress/regress0/arith/mod.01.smt2 +++ b/test/regress/regress0/arith/mod.01.smt2 @@ -1,6 +1,6 @@ ; 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/regress0/arith/mult.01.smt2 b/test/regress/regress0/arith/mult.01.smt2 index 4e2956d9d..8042e3cab 100644 --- a/test/regress/regress0/arith/mult.01.smt2 +++ b/test/regress/regress0/arith/mult.01.smt2 @@ -1,6 +1,6 @@ ; EXPECT: unsat (set-logic QF_NRA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :status unsat) (declare-fun n () Real) (declare-fun x () Real) diff --git a/test/regress/regress0/arrays/arrays0.smt2 b/test/regress/regress0/arrays/arrays0.smt2 index 652ff0bcb..ffc7d3e8f 100644 --- a/test/regress/regress0/arrays/arrays0.smt2 +++ b/test/regress/regress0/arrays/arrays0.smt2 @@ -8,7 +8,7 @@ http://www.ai.dist.unige.it/pdpar05/ |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status unsat) (declare-sort Index 0) diff --git a/test/regress/regress0/arrays/arrays1.smt2 b/test/regress/regress0/arrays/arrays1.smt2 index f001cc33e..6f6773916 100644 --- a/test/regress/regress0/arrays/arrays1.smt2 +++ b/test/regress/regress0/arrays/arrays1.smt2 @@ -8,7 +8,7 @@ http://www.ai.dist.unige.it/pdpar05/ |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status unsat) (declare-sort Index 0) diff --git a/test/regress/regress0/arrays/arrays2.smt2 b/test/regress/regress0/arrays/arrays2.smt2 index 7c14477e2..7e89ad6b2 100644 --- a/test/regress/regress0/arrays/arrays2.smt2 +++ b/test/regress/regress0/arrays/arrays2.smt2 @@ -8,7 +8,7 @@ http://www.ai.dist.unige.it/pdpar05/ |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-sort Index 0) diff --git a/test/regress/regress0/arrays/arrays3.smt2 b/test/regress/regress0/arrays/arrays3.smt2 index a21397b1d..aecfeee08 100644 --- a/test/regress/regress0/arrays/arrays3.smt2 +++ b/test/regress/regress0/arrays/arrays3.smt2 @@ -8,7 +8,7 @@ http://www.ai.dist.unige.it/pdpar05/ |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-sort Index 0) diff --git a/test/regress/regress0/arrays/arrays4.smt2 b/test/regress/regress0/arrays/arrays4.smt2 index f4afded65..e9acd5304 100644 --- a/test/regress/regress0/arrays/arrays4.smt2 +++ b/test/regress/regress0/arrays/arrays4.smt2 @@ -8,7 +8,7 @@ http://www.ai.dist.unige.it/pdpar05/ |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status unsat) (declare-sort Index 0) diff --git a/test/regress/regress0/aufbv/bug580.delta.smt2 b/test/regress/regress0/aufbv/bug580.delta.smt2 index bc9a66f9c..b06be7ea7 100644 --- a/test/regress/regress0/aufbv/bug580.delta.smt2 +++ b/test/regress/regress0/aufbv/bug580.delta.smt2 @@ -1,5 +1,5 @@ (set-info :source |fuzzsmt|) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "random") (set-info :status sat) (set-logic QF_AUFBV) diff --git a/test/regress/regress0/auflia/bug336.smt2 b/test/regress/regress0/auflia/bug336.smt2 index f8909c23c..34af91c6c 100644 --- a/test/regress/regress0/auflia/bug336.smt2 +++ b/test/regress/regress0/auflia/bug336.smt2 @@ -2,7 +2,7 @@ (set-info :source | This is based on an example in Section 6.2 of "A Decision Procedure for an Extensional Theory of Arrays" by Stump, Barrett, Dill, and Levitt. |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "check") (set-info :status unsat) (set-info :notes |This benchmark is designed to require an array DP to propagate a properly entailed disjunction of equalities between shared terms.|) diff --git a/test/regress/regress0/bt-test-00.smt2 b/test/regress/regress0/bt-test-00.smt2 index 517806542..167fb6323 100644 --- a/test/regress/regress0/bt-test-00.smt2 +++ b/test/regress/regress0/bt-test-00.smt2 @@ -1,6 +1,6 @@ ; EXPECT: unsat (set-logic QF_UF) -(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/bt-test-01.smt2 b/test/regress/regress0/bt-test-01.smt2 index e17bd2d7a..0b2b8b9f9 100644 --- a/test/regress/regress0/bt-test-01.smt2 +++ b/test/regress/regress0/bt-test-01.smt2 @@ -1,6 +1,6 @@ ; EXPECT: unsat (set-logic QF_UF) -(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/bug365.smt2 b/test/regress/regress0/bug365.smt2 index 6dd48a849..9c9ac8244 100644 --- a/test/regress/regress0/bug365.smt2 +++ b/test/regress/regress0/bug365.smt2 @@ -1,5 +1,5 @@ (set-logic QF_LIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :status unsat) (assert (let ((a 2)) diff --git a/test/regress/regress0/bug578.smt2 b/test/regress/regress0/bug578.smt2 index a4d53f8bf..f0e204310 100644 --- a/test/regress/regress0/bug578.smt2 +++ b/test/regress/regress0/bug578.smt2 @@ -1,4 +1,4 @@ -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :status sat) (set-logic QF_BV) (declare-fun v0 () (_ BitVec 1)) diff --git a/test/regress/regress0/buggy-ite.smt2 b/test/regress/regress0/buggy-ite.smt2 index 79e91b55e..5eac7700f 100644 --- a/test/regress/regress0/buggy-ite.smt2 +++ b/test/regress/regress0/buggy-ite.smt2 @@ -2,7 +2,7 @@ ; removal for PARAMETERIZED kinds. ; Thanks to Andrew Reynolds for catching this. (set-logic QF_UF) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :status sat) (declare-sort U 0) (declare-fun a () U) 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)) diff --git a/test/regress/regress0/decision/quant-ex1.smt2 b/test/regress/regress0/decision/quant-ex1.smt2 index 749b0e218..3bb3d5999 100644 --- a/test/regress/regress0/decision/quant-ex1.smt2 +++ b/test/regress/regress0/decision/quant-ex1.smt2 @@ -2,7 +2,7 @@ ; EXPECT: sat (set-logic AUFLIRA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "industrial") (set-info :status sat) (declare-sort U 0) diff --git a/test/regress/regress0/fmf/bug652.smt2 b/test/regress/regress0/fmf/bug652.smt2 deleted file mode 100644 index 13748eeea..000000000 --- a/test/regress/regress0/fmf/bug652.smt2 +++ /dev/null @@ -1,22 +0,0 @@ -; COMMAND-LINE: --fmf-fun --no-check-models -; EXPECT: sat -(set-logic UFDTSLIA) -(set-info :smt-lib-version 2.5) -(set-option :produce-models true) - -(declare-datatypes () ( - (List_boolean (List_boolean$CNil_boolean) (List_boolean$Cstr_boolean (List_boolean$Cstr_boolean$head Bool) (List_boolean$Cstr_boolean$tail List_boolean))) -) ) - -(define-funs-rec - ( - (f4208$lengthList_boolean((x List_boolean)) Int) - ) - ( - (ite (is-List_boolean$CNil_boolean x) 0 (+ 1 (f4208$lengthList_boolean (List_boolean$Cstr_boolean$tail x)))) - ) -) - - -(declare-const boolean Bool) -(check-sat) diff --git a/test/regress/regress0/fp/down-cast-RNA.smt2 b/test/regress/regress0/fp/down-cast-RNA.smt2 index 9509259a4..dc99ff144 100644 --- a/test/regress/regress0/fp/down-cast-RNA.smt2 +++ b/test/regress/regress0/fp/down-cast-RNA.smt2 @@ -4,7 +4,7 @@ (set-logic QF_FP) (set-info :source |Written by Andres Noetzli for issue #2183|) -(set-info :smt-lib-version 2.5) +(set-info :smt-lib-version 2.6) (set-info :category crafted) (set-info :status unsat) diff --git a/test/regress/regress0/fp/rti_3_5_bug.smt2 b/test/regress/regress0/fp/rti_3_5_bug.smt2 index 56c11bbf5..2c837b415 100644 --- a/test/regress/regress0/fp/rti_3_5_bug.smt2 +++ b/test/regress/regress0/fp/rti_3_5_bug.smt2 @@ -4,7 +4,7 @@ (set-logic QF_FP)
(set-info :source |Written by Martin for issue #2932|)
-(set-info :smt-lib-version 2.5)
+(set-info :smt-lib-version 2.6)
(set-info :category crafted)
(set-info :status unsat)
diff --git a/test/regress/regress0/get-value-incremental.smt2 b/test/regress/regress0/get-value-incremental.smt2 index c45cced82..6c3ee89ab 100644 --- a/test/regress/regress0/get-value-incremental.smt2 +++ b/test/regress/regress0/get-value-incremental.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --incremental ; EXPECT: sat ; EXPECT: (((f 0) 1)) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-option :produce-models true) (set-logic QF_UFLIA) diff --git a/test/regress/regress0/get-value-ints.smt2 b/test/regress/regress0/get-value-ints.smt2 index 97d8d1176..5434e3746 100644 --- a/test/regress/regress0/get-value-ints.smt2 +++ b/test/regress/regress0/get-value-ints.smt2 @@ -1,6 +1,6 @@ ; EXPECT: sat ; EXPECT: ((pos 1) (zero 0) (neg (- 6))) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-option :produce-models true) (set-logic QF_LIA) diff --git a/test/regress/regress0/get-value-reals-ints.smt2 b/test/regress/regress0/get-value-reals-ints.smt2 index e155255e7..8951cc797 100644 --- a/test/regress/regress0/get-value-reals-ints.smt2 +++ b/test/regress/regress0/get-value-reals-ints.smt2 @@ -1,6 +1,6 @@ ; EXPECT: sat ; EXPECT: ((pos_int 5) (pos_real_int_value 3.0) (pos_rat (/ 1 3)) (zero 0.0) (neg_rat (/ (- 2) 3)) (neg_real_int_value (- 2.0)) (neg_int (- 6))) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-option :produce-models true) (set-logic QF_LIRA) diff --git a/test/regress/regress0/get-value-reals.smt2 b/test/regress/regress0/get-value-reals.smt2 index 5d5319955..553c5ed72 100644 --- a/test/regress/regress0/get-value-reals.smt2 +++ b/test/regress/regress0/get-value-reals.smt2 @@ -1,6 +1,6 @@ ; EXPECT: sat ; EXPECT: ((pos_int 3.0) (pos_rat (/ 1 3)) (zero 0.0) (neg_rat (/ (- 2) 3)) (neg_int (- 2.0))) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-option :produce-models true) (set-logic QF_LRA) diff --git a/test/regress/regress0/hung10_itesdk_output1.smt2 b/test/regress/regress0/hung10_itesdk_output1.smt2 index 8bcdfdfbc..2dcbf1fcd 100644 --- a/test/regress/regress0/hung10_itesdk_output1.smt2 +++ b/test/regress/regress0/hung10_itesdk_output1.smt2 @@ -1,6 +1,6 @@ ( set-logic QF_ALL_SUPPORTED) ( set-info :source | SMT-COMP'06 organizers |) -( set-info :smt-lib-version 2.0) +( set-info :smt-lib-version 2.6) ( set-info :category "check") ( set-info :status sat) ( declare-fun x1 () Bool) diff --git a/test/regress/regress0/hung13sdk_output1.smt2 b/test/regress/regress0/hung13sdk_output1.smt2 index bf3ab9a26..7886153b0 100644 --- a/test/regress/regress0/hung13sdk_output1.smt2 +++ b/test/regress/regress0/hung13sdk_output1.smt2 @@ -1,6 +1,6 @@ ( set-logic QF_ALL_SUPPORTED) ( set-info :source | SMT-COMP'06 organizers |) -( set-info :smt-lib-version 2.0) +( set-info :smt-lib-version 2.6) ( set-info :category "check") ( set-info :status sat) ( declare-fun x1 () Bool) diff --git a/test/regress/regress0/lang_opts_2_5.smt2 b/test/regress/regress0/lang_opts_2_5.smt2 deleted file mode 100644 index 5a56960f0..000000000 --- a/test/regress/regress0/lang_opts_2_5.smt2 +++ /dev/null @@ -1,7 +0,0 @@ -; Check that the language set in the command line options has higher priority -; than the language specified in the input file. -; -; COMMAND-LINE: --lang=smt2.5 -; EXPECT: "LANG_SMTLIB_V2_5" -(set-info :smt-lib-version 2.6) -(get-option :input-language) diff --git a/test/regress/regress0/nl/magnitude-wrong-1020-m.smt2 b/test/regress/regress0/nl/magnitude-wrong-1020-m.smt2 index 9411224e5..6575385d5 100644 --- a/test/regress/regress0/nl/magnitude-wrong-1020-m.smt2 +++ b/test/regress/regress0/nl/magnitude-wrong-1020-m.smt2 @@ -7,7 +7,7 @@ From termination analysis of term rewriting. Submitted by Harald Roman Zankl <Harald.Zankl@uibk.ac.at> |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "industrial") (set-info :status sat) (define-fun x6 () Real diff --git a/test/regress/regress0/nl/very-easy-sat.smt2 b/test/regress/regress0/nl/very-easy-sat.smt2 index 06efa5806..0a0405a8e 100644 --- a/test/regress/regress0/nl/very-easy-sat.smt2 +++ b/test/regress/regress0/nl/very-easy-sat.smt2 @@ -18,7 +18,7 @@ Submitted by Dejan Jovanovic for SMT-LIB. |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "industrial") (set-info :status sat) (declare-fun skoC () Real) diff --git a/test/regress/regress0/nl/very-simple-unsat.smt2 b/test/regress/regress0/nl/very-simple-unsat.smt2 index e23d2d542..839fbb88b 100644 --- a/test/regress/regress0/nl/very-simple-unsat.smt2 +++ b/test/regress/regress0/nl/very-simple-unsat.smt2 @@ -5,7 +5,7 @@ Harald Roman Zankl <Harald.Zankl@uibk.ac.at> |) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status unsat) (declare-fun a () Real) diff --git a/test/regress/regress0/parser/as.smt2 b/test/regress/regress0/parser/as.smt2 index 2ba689541..2dc5c0e45 100644 --- a/test/regress/regress0/parser/as.smt2 +++ b/test/regress/regress0/parser/as.smt2 @@ -1,5 +1,5 @@ (set-logic QF_UF) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-sort I 0) diff --git a/test/regress/regress0/parser/strings20.smt2 b/test/regress/regress0/parser/strings20.smt2 index 3682e06e6..48e1113ea 100644 --- a/test/regress/regress0/parser/strings20.smt2 +++ b/test/regress/regress0/parser/strings20.smt2 @@ -1,15 +1,15 @@ ; EXPECT: sat ; EXPECT: ( -; EXPECT: (define-fun s () String "\"") +; EXPECT: (define-fun s () String "\u{5c}""") ; EXPECT: ) (set-logic QF_S) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-option :produce-models true) (declare-fun s () String) -(assert (= s "\"")) +(assert (= s "\""")) (check-sat) (get-model) diff --git a/test/regress/regress0/parser/strings25.smt2 b/test/regress/regress0/parser/strings25.smt2 index f8cc084e6..eac95dd5c 100644 --- a/test/regress/regress0/parser/strings25.smt2 +++ b/test/regress/regress0/parser/strings25.smt2 @@ -4,7 +4,6 @@ ; EXPECT: ) (set-logic QF_S) -(set-info :smt-lib-version 2.5) (set-option :produce-models true) (declare-fun s () String) diff --git a/test/regress/regress0/push-pop/bug691.smt2 b/test/regress/regress0/push-pop/bug691.smt2 index df8964658..dd4e9ea09 100644 --- a/test/regress/regress0/push-pop/bug691.smt2 +++ b/test/regress/regress0/push-pop/bug691.smt2 @@ -2,12 +2,9 @@ ; EXPECT: sat ; EXPECT: sat (set-logic UFDTSLIA) -(set-info :smt-lib-version 2.5) - -(declare-datatypes () ( - (Response (Response$Response (Response$Response$success Bool))) - ) ) +(set-info :smt-lib-version 2.6) +(declare-datatype Response ((Response$Response (Response$Response$success Bool)))) (push 1) (declare-fun $BLout$3248$0$1$() Response) 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) diff --git a/test/regress/regress0/strings/bug001.smt2 b/test/regress/regress0/strings/bug001.smt2 index a8d2d8992..751cacd8f 100644 --- a/test/regress/regress0/strings/bug001.smt2 +++ b/test/regress/regress0/strings/bug001.smt2 @@ -1,4 +1,4 @@ -(set-info :smt-lib-version 2.5) +(set-info :smt-lib-version 2.6) (set-logic QF_S) (set-info :status sat) @@ -6,10 +6,10 @@ (declare-fun y () String) (declare-fun z () String) -(assert (= "\x4a" x)) -(assert (= "\x6a" y)) +(assert (= "J" x)) +(assert (= "j" y)) -(assert (= "\x4A" z)) +(assert (= "J" z)) (assert (= x z)) diff --git a/test/regress/regress0/strings/bug002.smt2 b/test/regress/regress0/strings/bug002.smt2 index 5bf21ebb9..f35a5fffb 100644 --- a/test/regress/regress0/strings/bug002.smt2 +++ b/test/regress/regress0/strings/bug002.smt2 @@ -1,10 +1,10 @@ -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-logic ASLIA) (set-option :strings-exp true) (set-info :status sat) ; regex = [\*-,\t\*-\|](.{6,}()?)+ -(define-fun strinre ((?s String)) Bool (str.in.re ?s (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.union re.nostr (re.range "*" ",") (str.to.re "\t") (re.range "*" "|") ) (re.+ (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") ((_ re.^ 6) re.allchar) (re.opt (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") ) ) ) ) ) ) ) ) ) ) +(define-fun strinre ((?s String)) Bool (str.in_re ?s (re.union re.none (re.++ (str.to_re "") (str.to_re "") (re.union re.none (re.range "*" ",") (str.to_re "\t") (re.range "*" "|") ) (re.+ (re.union re.none (re.++ (str.to_re "") (str.to_re "") ((_ re.^ 6) re.allchar) (re.opt (re.union re.none (re.++ (str.to_re "") (str.to_re "") ) ) ) ) ) ) ) ) ) ) (assert (not (strinre "6O\1\127\n?"))) (check-sat) diff --git a/test/regress/regress0/strings/escchar.smt2 b/test/regress/regress0/strings/escchar.smt2 index 67a184ade..a8a7c242f 100644 --- a/test/regress/regress0/strings/escchar.smt2 +++ b/test/regress/regress0/strings/escchar.smt2 @@ -1,11 +1,11 @@ (set-logic QF_S) (set-info :status sat) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (declare-fun x () String) (declare-const I Int) -(assert (= x "\0\1\2\3\04\005\x06\7\8\9ABC\\\"\t\a\b")) +(assert (= x "\0\1\2\3\04\005\x06\7\8\9ABC\\""\t\a\b")) (assert (= I (str.len x))) diff --git a/test/regress/regress0/uflia/check01.smt2 b/test/regress/regress0/uflia/check01.smt2 index 33be9346a..f182c5fbe 100644 --- a/test/regress/regress0/uflia/check01.smt2 +++ b/test/regress/regress0/uflia/check01.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --incremental ; EXPECT: sat (set-logic QF_UFLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :status sat) (declare-fun f (Int) Bool) diff --git a/test/regress/regress0/unconstrained/arith.smt2 b/test/regress/regress0/unconstrained/arith.smt2 index 3dfab3b0e..fd951c7ab 100644 --- a/test/regress/regress0/unconstrained/arith.smt2 +++ b/test/regress/regress0/unconstrained/arith.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun v1 () Int) diff --git a/test/regress/regress0/unconstrained/arith2.smt2 b/test/regress/regress0/unconstrained/arith2.smt2 index d6206287a..bf9f34298 100644 --- a/test/regress/regress0/unconstrained/arith2.smt2 +++ b/test/regress/regress0/unconstrained/arith2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFLIRA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status unsat) (declare-fun v1 () Int) diff --git a/test/regress/regress0/unconstrained/arith3.smt2 b/test/regress/regress0/unconstrained/arith3.smt2 index fd24c3f65..edf0d4cdf 100644 --- a/test/regress/regress0/unconstrained/arith3.smt2 +++ b/test/regress/regress0/unconstrained/arith3.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFLIRA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status unsat) (declare-fun v1 () Int) diff --git a/test/regress/regress0/unconstrained/arith4.smt2 b/test/regress/regress0/unconstrained/arith4.smt2 index 507a18a78..f68ebf88a 100644 --- a/test/regress/regress0/unconstrained/arith4.smt2 +++ b/test/regress/regress0/unconstrained/arith4.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFNIRA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status unsat) (declare-fun v1 () Int) diff --git a/test/regress/regress0/unconstrained/arith5.smt2 b/test/regress/regress0/unconstrained/arith5.smt2 index 5e54083a5..cc19b5389 100644 --- a/test/regress/regress0/unconstrained/arith5.smt2 +++ b/test/regress/regress0/unconstrained/arith5.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLRA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun v1 () Real) diff --git a/test/regress/regress0/unconstrained/arith6.smt2 b/test/regress/regress0/unconstrained/arith6.smt2 index ce3630264..24e57b0f7 100644 --- a/test/regress/regress0/unconstrained/arith6.smt2 +++ b/test/regress/regress0/unconstrained/arith6.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLRA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun v1 () Real) diff --git a/test/regress/regress0/unconstrained/arith7.smt2 b/test/regress/regress0/unconstrained/arith7.smt2 index 105320632..5fe061803 100644 --- a/test/regress/regress0/unconstrained/arith7.smt2 +++ b/test/regress/regress0/unconstrained/arith7.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFLIRA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status unsat) (declare-fun v1 () Int) diff --git a/test/regress/regress0/unconstrained/array1.smt2 b/test/regress/regress0/unconstrained/array1.smt2 index f1acfa759..5c8ff5147 100644 --- a/test/regress/regress0/unconstrained/array1.smt2 +++ b/test/regress/regress0/unconstrained/array1.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBV) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun v1 () (_ BitVec 16)) diff --git a/test/regress/regress0/unconstrained/bvbool.smt2 b/test/regress/regress0/unconstrained/bvbool.smt2 index b1943124e..9964aa728 100644 --- a/test/regress/regress0/unconstrained/bvbool.smt2 +++ b/test/regress/regress0/unconstrained/bvbool.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvbool2.smt2 b/test/regress/regress0/unconstrained/bvbool2.smt2 index 49b7d5fc8..788a0578b 100644 --- a/test/regress/regress0/unconstrained/bvbool2.smt2 +++ b/test/regress/regress0/unconstrained/bvbool2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status unsat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvbool3.smt2 b/test/regress/regress0/unconstrained/bvbool3.smt2 index f24b129e0..524fdd107 100644 --- a/test/regress/regress0/unconstrained/bvbool3.smt2 +++ b/test/regress/regress0/unconstrained/bvbool3.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvcmp.smt2 b/test/regress/regress0/unconstrained/bvcmp.smt2 index ae50d350c..5a6c314bd 100644 --- a/test/regress/regress0/unconstrained/bvcmp.smt2 +++ b/test/regress/regress0/unconstrained/bvcmp.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun v1 () (_ BitVec 1)) diff --git a/test/regress/regress0/unconstrained/bvconcat.smt2 b/test/regress/regress0/unconstrained/bvconcat.smt2 index 6f4e38ec7..c93189837 100644 --- a/test/regress/regress0/unconstrained/bvconcat.smt2 +++ b/test/regress/regress0/unconstrained/bvconcat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvconcat2.smt2 b/test/regress/regress0/unconstrained/bvconcat2.smt2 index 789e4c6c8..9e9ac87d3 100644 --- a/test/regress/regress0/unconstrained/bvconcat2.smt2 +++ b/test/regress/regress0/unconstrained/bvconcat2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status unsat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvdiv.smt2 b/test/regress/regress0/unconstrained/bvdiv.smt2 index 990a8d457..2c2b4d5f8 100644 --- a/test/regress/regress0/unconstrained/bvdiv.smt2 +++ b/test/regress/regress0/unconstrained/bvdiv.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvext.smt2 b/test/regress/regress0/unconstrained/bvext.smt2 index b31efe3aa..dd4de7251 100644 --- a/test/regress/regress0/unconstrained/bvext.smt2 +++ b/test/regress/regress0/unconstrained/bvext.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun v1 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvite.smt2 b/test/regress/regress0/unconstrained/bvite.smt2 index 3cac4670b..f89dd6b6b 100644 --- a/test/regress/regress0/unconstrained/bvite.smt2 +++ b/test/regress/regress0/unconstrained/bvite.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvmul.smt2 b/test/regress/regress0/unconstrained/bvmul.smt2 index a109d9471..c26304073 100644 --- a/test/regress/regress0/unconstrained/bvmul.smt2 +++ b/test/regress/regress0/unconstrained/bvmul.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvmul2.smt2 b/test/regress/regress0/unconstrained/bvmul2.smt2 index 4e413c24f..fd8cc1e3d 100644 --- a/test/regress/regress0/unconstrained/bvmul2.smt2 +++ b/test/regress/regress0/unconstrained/bvmul2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status unsat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvmul3.smt2 b/test/regress/regress0/unconstrained/bvmul3.smt2 index 71cf37371..e38944082 100644 --- a/test/regress/regress0/unconstrained/bvmul3.smt2 +++ b/test/regress/regress0/unconstrained/bvmul3.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvnot.smt2 b/test/regress/regress0/unconstrained/bvnot.smt2 index 4f62d2a0d..cdeb77a3b 100644 --- a/test/regress/regress0/unconstrained/bvnot.smt2 +++ b/test/regress/regress0/unconstrained/bvnot.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun v1 () (_ BitVec 1)) diff --git a/test/regress/regress0/unconstrained/bvsle.smt2 b/test/regress/regress0/unconstrained/bvsle.smt2 index 391a6c9d7..594ed0c4d 100644 --- a/test/regress/regress0/unconstrained/bvsle.smt2 +++ b/test/regress/regress0/unconstrained/bvsle.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvsle2.smt2 b/test/regress/regress0/unconstrained/bvsle2.smt2 index f23b119fe..fe4c4d4b4 100644 --- a/test/regress/regress0/unconstrained/bvsle2.smt2 +++ b/test/regress/regress0/unconstrained/bvsle2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvsle3.smt2 b/test/regress/regress0/unconstrained/bvsle3.smt2 index 2887cdca8..5d8359e31 100644 --- a/test/regress/regress0/unconstrained/bvsle3.smt2 +++ b/test/regress/regress0/unconstrained/bvsle3.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status unsat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvsle4.smt2 b/test/regress/regress0/unconstrained/bvsle4.smt2 index 289104ec8..0c60acfcb 100644 --- a/test/regress/regress0/unconstrained/bvsle4.smt2 +++ b/test/regress/regress0/unconstrained/bvsle4.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvsle5.smt2 b/test/regress/regress0/unconstrained/bvsle5.smt2 index cbe15db58..e8027465f 100644 --- a/test/regress/regress0/unconstrained/bvsle5.smt2 +++ b/test/regress/regress0/unconstrained/bvsle5.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status unsat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvslt.smt2 b/test/regress/regress0/unconstrained/bvslt.smt2 index 2e20460c5..191038a4c 100644 --- a/test/regress/regress0/unconstrained/bvslt.smt2 +++ b/test/regress/regress0/unconstrained/bvslt.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvslt2.smt2 b/test/regress/regress0/unconstrained/bvslt2.smt2 index 743cfbebe..a22e51cc6 100644 --- a/test/regress/regress0/unconstrained/bvslt2.smt2 +++ b/test/regress/regress0/unconstrained/bvslt2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvslt3.smt2 b/test/regress/regress0/unconstrained/bvslt3.smt2 index db1f3dcd9..e702379ac 100644 --- a/test/regress/regress0/unconstrained/bvslt3.smt2 +++ b/test/regress/regress0/unconstrained/bvslt3.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status unsat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvslt4.smt2 b/test/regress/regress0/unconstrained/bvslt4.smt2 index 9c696d48b..bdda57a8d 100644 --- a/test/regress/regress0/unconstrained/bvslt4.smt2 +++ b/test/regress/regress0/unconstrained/bvslt4.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvslt5.smt2 b/test/regress/regress0/unconstrained/bvslt5.smt2 index c5696f0a2..2dbe3645c 100644 --- a/test/regress/regress0/unconstrained/bvslt5.smt2 +++ b/test/regress/regress0/unconstrained/bvslt5.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status unsat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvule.smt2 b/test/regress/regress0/unconstrained/bvule.smt2 index d0678d87c..58e8f2796 100644 --- a/test/regress/regress0/unconstrained/bvule.smt2 +++ b/test/regress/regress0/unconstrained/bvule.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvule2.smt2 b/test/regress/regress0/unconstrained/bvule2.smt2 index 5dfa6c1b1..f3dd4860e 100644 --- a/test/regress/regress0/unconstrained/bvule2.smt2 +++ b/test/regress/regress0/unconstrained/bvule2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvule3.smt2 b/test/regress/regress0/unconstrained/bvule3.smt2 index e9892e598..e16baff02 100644 --- a/test/regress/regress0/unconstrained/bvule3.smt2 +++ b/test/regress/regress0/unconstrained/bvule3.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status unsat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvule4.smt2 b/test/regress/regress0/unconstrained/bvule4.smt2 index 0fccae301..564db9748 100644 --- a/test/regress/regress0/unconstrained/bvule4.smt2 +++ b/test/regress/regress0/unconstrained/bvule4.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvule5.smt2 b/test/regress/regress0/unconstrained/bvule5.smt2 index 4d4e0e95f..70ac8910f 100644 --- a/test/regress/regress0/unconstrained/bvule5.smt2 +++ b/test/regress/regress0/unconstrained/bvule5.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status unsat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvult.smt2 b/test/regress/regress0/unconstrained/bvult.smt2 index 9429237a4..44bdefd62 100644 --- a/test/regress/regress0/unconstrained/bvult.smt2 +++ b/test/regress/regress0/unconstrained/bvult.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvult2.smt2 b/test/regress/regress0/unconstrained/bvult2.smt2 index c86699b48..f8eee92f6 100644 --- a/test/regress/regress0/unconstrained/bvult2.smt2 +++ b/test/regress/regress0/unconstrained/bvult2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvult3.smt2 b/test/regress/regress0/unconstrained/bvult3.smt2 index ceb19ea75..43f79a569 100644 --- a/test/regress/regress0/unconstrained/bvult3.smt2 +++ b/test/regress/regress0/unconstrained/bvult3.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status unsat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvult4.smt2 b/test/regress/regress0/unconstrained/bvult4.smt2 index 04008c006..fe716b139 100644 --- a/test/regress/regress0/unconstrained/bvult4.smt2 +++ b/test/regress/regress0/unconstrained/bvult4.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/bvult5.smt2 b/test/regress/regress0/unconstrained/bvult5.smt2 index 53f76f0d3..151db6f02 100644 --- a/test/regress/regress0/unconstrained/bvult5.smt2 +++ b/test/regress/regress0/unconstrained/bvult5.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status unsat) (declare-fun x0 () (_ BitVec 10)) diff --git a/test/regress/regress0/unconstrained/geq.smt2 b/test/regress/regress0/unconstrained/geq.smt2 index d3bcc506f..e84876133 100644 --- a/test/regress/regress0/unconstrained/geq.smt2 +++ b/test/regress/regress0/unconstrained/geq.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun v1 () Int) diff --git a/test/regress/regress0/unconstrained/gt.smt2 b/test/regress/regress0/unconstrained/gt.smt2 index d4d6d4a5d..2c118cd9c 100644 --- a/test/regress/regress0/unconstrained/gt.smt2 +++ b/test/regress/regress0/unconstrained/gt.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun v1 () Int) diff --git a/test/regress/regress0/unconstrained/leq.smt2 b/test/regress/regress0/unconstrained/leq.smt2 index 4eea4df9c..ed568c5fd 100644 --- a/test/regress/regress0/unconstrained/leq.smt2 +++ b/test/regress/regress0/unconstrained/leq.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun v1 () Int) diff --git a/test/regress/regress0/unconstrained/lt.smt2 b/test/regress/regress0/unconstrained/lt.smt2 index a0a42f4ef..06724ad45 100644 --- a/test/regress/regress0/unconstrained/lt.smt2 +++ b/test/regress/regress0/unconstrained/lt.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun v1 () Int) diff --git a/test/regress/regress0/unconstrained/uf1.smt2 b/test/regress/regress0/unconstrained/uf1.smt2 index 3e28c2f8b..f85054926 100644 --- a/test/regress/regress0/unconstrained/uf1.smt2 +++ b/test/regress/regress0/unconstrained/uf1.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun v1 () Int) diff --git a/test/regress/regress0/unconstrained/xor.smt2 b/test/regress/regress0/unconstrained/xor.smt2 index fcc66b015..cb0b39040 100644 --- a/test/regress/regress0/unconstrained/xor.smt2 +++ b/test/regress/regress0/unconstrained/xor.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --unconstrained-simp --no-check-models (set-logic QF_AUFBVLIA) -(set-info :smt-lib-version 2.0) +(set-info :smt-lib-version 2.6) (set-info :category "crafted") (set-info :status sat) (declare-fun x0 () (_ BitVec 10)) |