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))