16 files changed, 190 insertions, 3 deletions
diff --git a/test/regress/regress1/bags/fuzzy1.smt2 b/test/regress/regress1/bags/fuzzy1.smt2
new file mode 100644
index 000000000..f9fee0ec4
--- /dev/null
+++ b/test/regress/regress1/bags/fuzzy1.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () (Bag (Tuple Int Int)))
+(declare-fun b () (Bag (Tuple Int Int)))
+(declare-fun c () Int) ; c here is zero
+(assert
+  (and
+    (= b (difference_subtract b a)) ; b is empty
+    (= a (bag (tuple c 0) 1)))) ; a = {|(<0, 0>, 1)|}
+(check-sat)
diff --git a/test/regress/regress1/bags/fuzzy2.smt2 b/test/regress/regress1/bags/fuzzy2.smt2
new file mode 100644
index 000000000..31da47f53
--- /dev/null
+++ b/test/regress/regress1/bags/fuzzy2.smt2
@@ -0,0 +1,15 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () (Bag (Tuple Int Int)))
+(declare-fun b () (Bag (Tuple Int Int)))
+(declare-fun c () Int)
+(declare-fun d () (Tuple Int Int))
+(assert
+  (let ((D (bag d c))) ; when c = zero, then D is empty
+    (and
+      (= a (bag (tuple 1 1) c)) ; when c = zero, then a is empty
+      (= a (union_max a D))
+      (= a (difference_subtract a (bag d 1)))
+      (= a (union_disjoint a D))
+      (= a (intersection_min a D)))))
+(check-sat)
diff --git a/test/regress/regress1/bags/map.smt2 b/test/regress/regress1/bags/map1.smt2
index 54d671415..54d671415 100644
--- a/test/regress/regress1/bags/map.smt2
+++ b/test/regress/regress1/bags/map1.smt2
diff --git a/test/regress/regress1/bags/map2.smt2 b/test/regress/regress1/bags/map2.smt2
new file mode 100644
index 000000000..faed04caa
--- /dev/null
+++ b/test/regress/regress1/bags/map2.smt2
@@ -0,0 +1,9 @@
+(set-logic HO_ALL)
+(set-info :status sat)
+(set-option :fmf-bound true)
+(declare-fun A () (Bag Int))
+(declare-fun B () (Bag Int))
+(declare-fun f (Int) Int)
+(assert (= B (bag.map f A)))
+(assert (= (bag.count (- 2) B) 57))
+(check-sat)
diff --git a/test/regress/regress1/bags/map3.smt2 b/test/regress/regress1/bags/map3.smt2
new file mode 100644
index 000000000..637815fa5
--- /dev/null
+++ b/test/regress/regress1/bags/map3.smt2
@@ -0,0 +1,10 @@
+(set-logic HO_ALL)
+(set-info :status unsat)
+(set-option :fmf-bound true)
+(declare-fun A () (Bag Int))
+(declare-fun B () (Bag Int))
+(define-fun f ((x Int)) Int (+ x 1))
+(assert (= B (bag.map f A)))
+(assert (= (bag.count (- 2) B) 57))
+(assert (= A (as emptybag (Bag Int)) ))
+(check-sat)
diff --git a/test/regress/regress1/ho/issue4758.smt2 b/test/regress/regress1/ho/issue4758.smt2
new file mode 100644
index 000000000..dab284c11
--- /dev/null
+++ b/test/regress/regress1/ho/issue4758.smt2
@@ -0,0 +1,6 @@
+(set-logic HO_ALL)
+(set-info :status sat)
+(declare-fun a () Real)
+(declare-fun b (Real Real) Real)
+(assert (> (b a 0) (b (- a) 1)))
+(check-sat)
diff --git a/test/regress/regress1/ho/issue5078-small.smt2 b/test/regress/regress1/ho/issue5078-small.smt2
new file mode 100644
index 000000000..21077434a
--- /dev/null
+++ b/test/regress/regress1/ho/issue5078-small.smt2
@@ -0,0 +1,8 @@
+(set-logic HO_QF_UFLIA)
+(set-info :status sat)
+(declare-fun a (Int Int) Int)
+(declare-fun d () Int)
+(declare-fun e () Int)
+(assert (= (a d 0) (a 0 1)))
+(assert (= d (mod e 3)))
+(check-sat)
diff --git a/test/regress/regress1/ho/issue5201-1.smt2 b/test/regress/regress1/ho/issue5201-1.smt2
new file mode 100644
index 000000000..9f6e058da
--- /dev/null
+++ b/test/regress/regress1/ho/issue5201-1.smt2
@@ -0,0 +1,20 @@
+(set-logic HO_QF_UFLIA)
+(set-info :status sat)
+(declare-fun a () Int)
+(declare-fun b (Int Int) Int)
+(declare-fun c (Int Int) Int)
+(declare-fun d () Int)
+(declare-fun e () Int)
+(declare-fun f () Int)
+(declare-fun g () Int)
+(declare-fun i () Int)
+(declare-fun j () Int)
+(declare-fun k () Int)
+(assert (= d (b j d) a))
+(assert (= e (c e i)))
+(assert (= (b k f) a))
+(assert (= d (+ g 4)))
+(assert (= j (* g 5)))
+(assert (= e (+ g 5)))
+(assert (= k 0))
+(check-sat)
diff --git a/test/regress/regress1/proofs/qgu-fuzz-arrays-1-dd-te-auto.smt2 b/test/regress/regress1/proofs/qgu-fuzz-arrays-1-dd-te-auto.smt2
new file mode 100644
index 000000000..b55fb3d49
--- /dev/null
+++ b/test/regress/regress1/proofs/qgu-fuzz-arrays-1-dd-te-auto.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-const x Int)
+(declare-fun b () (Array Int Int))
+(declare-fun y () Int)
+(assert (and (= b (store b x y)) (= b (store b y y)) (= y (ite (> y 0) 0 y)) (= (store b 0 0) (store (store b y 1) 1 1))))
+(check-sat)
diff --git a/test/regress/regress1/push-pop/arith_lra_01.smt2 b/test/regress/regress1/push-pop/arith_lra_01.smt2
index 02e22d685..b16bbdda0 100644
--- a/test/regress/regress1/push-pop/arith_lra_01.smt2
+++ b/test/regress/regress1/push-pop/arith_lra_01.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --no-produce-proofs
+; COMMAND-LINE: --incremental
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: sat
diff --git a/test/regress/regress1/push-pop/fuzz_3_6.smt2 b/test/regress/regress1/push-pop/fuzz_3_6.smt2
index 4ad684402..1901016c2 100644
--- a/test/regress/regress1/push-pop/fuzz_3_6.smt2
+++ b/test/regress/regress1/push-pop/fuzz_3_6.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --no-produce-proofs
+; COMMAND-LINE: --incremental
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: unsat
diff --git a/test/regress/regress1/quantifiers/issue7385-sygus-inst-i.smt2 b/test/regress/regress1/quantifiers/issue7385-sygus-inst-i.smt2
new file mode 100644
index 000000000..26fc1cf7e
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue7385-sygus-inst-i.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: -i
+; EXPECT: sat
+(set-logic NIRA)
+(push)
+(assert (exists ((q29 Int) (q30 Bool) (q35 Bool)) (= (= 0 q29) (= q35 q30))))
+(push)
+(pop)
+(pop)
+(check-sat)
diff --git a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
index 7249e87aa..465408cc5 100644
--- a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
+++ b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-unsat-cores --no-produce-proofs
+; COMMAND-LINE: --no-check-unsat-cores
 ; EXPECT: unsat
 
 ; Note we require disabling proofs/unsat cores due to timeouts in nightlies
diff --git a/test/regress/regress1/strings/issue6766-re-elim-bv.smt2 b/test/regress/regress1/strings/issue6766-re-elim-bv.smt2
new file mode 100644
index 000000000..13677838b
--- /dev/null
+++ b/test/regress/regress1/strings/issue6766-re-elim-bv.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () String)
+(declare-fun b () String)
+(assert
+ (str.in_re (str.++ a (ite (str.in_re (str.++ a "BA" b) (re.++ (re.* (str.to_re "A")) (str.to_re "B"))) b a))
+  (re.diff (re.* (str.to_re "A")) (str.to_re ""))))
+(check-sat)
diff --git a/test/regress/regress1/strings/non-terminating-rewrite-aent.smt2 b/test/regress/regress1/strings/non-terminating-rewrite-aent.smt2
new file mode 100644
index 000000000..211209255
--- /dev/null
+++ b/test/regress/regress1/strings/non-terminating-rewrite-aent.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () String)
+(declare-fun b () String)
+(declare-fun c () String)
+(assert 
+(let ((_let_1 (str.len a))) (let ((_let_2 (str.len b))) (let ((_let_3 (+ _let_1 (* (- 1) _let_2)))) (let ((_let_4 (ite (>= _let_3 1) (str.substr a 0 _let_3) (str.substr b 0 (+ (* (- 1) _let_1) _let_2))))) (let ((_let_5 (str.len _let_4))) (let ((_let_6 (str.len c))) (let ((_let_7 (+ _let_6 (* (- 1) _let_5)))) (let ((_let_8 (ite (>= _let_7 0) (str.substr c _let_5 _let_7) (str.substr _let_4 _let_6 (+ (* (- 1) _let_6) _let_5))))) (let ((_let_9 (str.len _let_8))) (let ((_let_10 (ite (>= _let_1 _let_9) (str.substr a _let_9 (- _let_1 _let_9)) (str.substr _let_8 _let_1 (- _let_9 _let_1))))) (and (= _let_8 (str.++ a _let_10)) (not (= "" _let_10)) (>= (str.len _let_10) 1))))))))))))
+)
+(check-sat)
diff --git a/test/regress/regress1/strings/pattern1.smt2 b/test/regress/regress1/strings/pattern1.smt2
new file mode 100644
index 000000000..b75fdb9be
--- /dev/null
+++ b/test/regress/regress1/strings/pattern1.smt2
@@ -0,0 +1,73 @@
+(set-option :produce-models true)
+(set-logic QF_SLIA)
+(set-info :status sat)
+(declare-const x String)
+
+(assert
+ (str.in_re
+  x
+  (re.++
+   (str.to_re "pref")
+   (re.* re.allchar)
+   (str.to_re "a")
+   (re.* re.allchar)
+   (str.to_re "b")
+   (re.* re.allchar)
+   (str.to_re "c")
+   (re.* re.allchar)
+   (str.to_re "d")
+   (re.* re.allchar)
+   (str.to_re "e")
+   (re.* re.allchar)
+   (str.to_re "f")
+   (re.* re.allchar)
+   (str.to_re "g")
+   (re.* re.allchar)
+   (str.to_re "h")
+   (re.* re.allchar)
+   (str.to_re "i")
+   (re.* re.allchar)
+   (str.to_re "j")
+   (re.* re.allchar)
+   (str.to_re "k")
+   (re.* re.allchar)
+   (str.to_re "l")
+   (re.* re.allchar)
+   (str.to_re "m")
+   (re.* re.allchar)
+   (str.to_re "n")
+   (re.* re.allchar)
+   (str.to_re "o")
+   (re.* re.allchar)
+   (str.to_re "p")
+   (re.* re.allchar)
+   (str.to_re "q")
+   (re.* re.allchar)
+   (str.to_re "r")
+   (re.* re.allchar)
+   (str.to_re "s")
+   (re.* re.allchar)
+   (str.to_re "t")
+   (re.* re.allchar)
+   (str.to_re "u")
+   (re.* re.allchar)
+   (str.to_re "v")
+   (re.* re.allchar)
+   (str.to_re "w")
+   (re.* re.allchar)
+   (str.to_re "x")
+   (re.* re.allchar)
+   (str.to_re "y")
+   (re.* re.allchar)
+   (str.to_re "z")
+   (re.* re.allchar))))
+
+(assert
+ (or
+  (= x "pref0a-b-c-de")
+  (str.in_re x (re.++ (str.to_re "prefix") (re.* re.allchar)))
+  (str.in_re x (re.++ (re.* re.allchar) (str.to_re "test") (re.* re.allchar)))))
+
+(check-sat)
+
+