10 files changed, 129 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 10e2f414e..5f82aedf1 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -861,6 +861,15 @@ set(regress_0_tests
   regress0/sep/skolem_emp.smt2
   regress0/sep/trees-1.smt2
   regress0/sep/wand-crash.smt2
+  regress0/seq/seq-2var.smt2
+  regress0/seq/seq-ex1.smt2
+  regress0/seq/seq-ex2.smt2
+  regress0/seq/seq-ex3.smt2
+  regress0/seq/seq-ex4.smt2
+  regress0/seq/seq-ex5-dd.smt2
+  regress0/seq/seq-ex5.smt2
+  regress0/seq/seq-nemp.smt2
+  regress0/seq/seq-rewrites.smt2
   regress0/sets/abt-min.smt2
   regress0/sets/abt-te-exh.smt2
   regress0/sets/abt-te-exh2.smt2
diff --git a/test/regress/regress0/seq/seq-2var.smt2 b/test/regress/regress0/seq/seq-2var.smt2
new file mode 100644
index 000000000..3a0d8934f
--- /dev/null
+++ b/test/regress/regress0/seq/seq-2var.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_SLIA)
+(set-info :status sat)
+(declare-fun x () (Seq Int))
+(declare-fun y () (Seq Int))
+
+(assert (not (= x y)))
+
+(check-sat)
diff --git a/test/regress/regress0/seq/seq-ex1.smt2 b/test/regress/regress0/seq/seq-ex1.smt2
new file mode 100644
index 000000000..817ee5f8e
--- /dev/null
+++ b/test/regress/regress0/seq/seq-ex1.smt2
@@ -0,0 +1,10 @@
+(set-logic QF_UFSLIA)
+(set-info :status sat)
+(declare-fun x () (Seq Int))
+(declare-fun y () (Seq Int))
+(declare-fun f ((Seq Int)) (Seq Bool))
+
+(assert (not (= x y)))
+(assert (not (= (f x) (f y))))
+
+(check-sat)
diff --git a/test/regress/regress0/seq/seq-ex2.smt2 b/test/regress/regress0/seq/seq-ex2.smt2
new file mode 100644
index 000000000..89b9d3100
--- /dev/null
+++ b/test/regress/regress0/seq/seq-ex2.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_SLIA)
+(set-info :status unsat)
+(declare-fun x () (Seq Int))
+(declare-fun y () (Seq Int))
+(declare-fun z () Int)
+(assert (> z 10))
+(assert (= (seq.len x) (seq.len y)))
+(assert (= (seq.++ x (seq.unit z)) (seq.++ y (seq.unit 5))))
+(check-sat)
diff --git a/test/regress/regress0/seq/seq-ex3.smt2 b/test/regress/regress0/seq/seq-ex3.smt2
new file mode 100644
index 000000000..abafdeddf
--- /dev/null
+++ b/test/regress/regress0/seq/seq-ex3.smt2
@@ -0,0 +1,18 @@
+(set-logic QF_SLIA)
+(set-info :status unsat)
+(declare-fun x () (Seq (Seq Int)))
+(declare-fun xp () (Seq (Seq Int)))
+(declare-fun y () (Seq (Seq Int)))
+(declare-fun yp () (Seq (Seq Int)))
+(declare-fun z () (Seq Int))
+(declare-fun w () (Seq Int))
+(declare-fun i () Int)
+(declare-fun j () Int)
+(declare-fun n () Int)
+(assert (> i j))
+(assert (= (seq.extract z n 1) (seq.unit i)))
+(assert (= (seq.extract w n 1) (seq.unit j)))
+(assert (= x (seq.++ (seq.unit z) xp)))
+(assert (= y (seq.++ (seq.unit w) yp)))
+(assert (= x y))
+(check-sat)
diff --git a/test/regress/regress0/seq/seq-ex4.smt2 b/test/regress/regress0/seq/seq-ex4.smt2
new file mode 100644
index 000000000..93fed72c7
--- /dev/null
+++ b/test/regress/regress0/seq/seq-ex4.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_SLIA)
+(set-info :status unsat)
+(declare-fun z () (Seq Int))
+(declare-fun i () Int)
+(declare-fun n () Int)
+(assert (= (seq.extract z n 1) (seq.unit i)))
+(assert (< (seq.len z) n))
+(check-sat)
diff --git a/test/regress/regress0/seq/seq-ex5-dd.smt2 b/test/regress/regress0/seq/seq-ex5-dd.smt2
new file mode 100644
index 000000000..d9ef5c8ba
--- /dev/null
+++ b/test/regress/regress0/seq/seq-ex5-dd.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_SLIA)
+(set-info :status sat)
+(declare-fun z () (Seq Int))
+(declare-fun i () Int)
+(declare-fun n () Int)
+(assert (> i 777))
+(assert (= (seq.extract z n 1) (seq.unit i)))
+(check-sat)
diff --git a/test/regress/regress0/seq/seq-ex5.smt2 b/test/regress/regress0/seq/seq-ex5.smt2
new file mode 100644
index 000000000..9fa72bc6b
--- /dev/null
+++ b/test/regress/regress0/seq/seq-ex5.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_SLIA)
+(set-option :strings-exp true)
+(set-info :status sat)
+(declare-fun z () (Seq Int))
+(declare-fun w () (Seq Int))
+(declare-fun i () Int)
+(assert (> i 777))
+(assert (not (= (seq.replace z (seq.unit i) w) z)))
+(check-sat)
diff --git a/test/regress/regress0/seq/seq-nemp.smt2 b/test/regress/regress0/seq/seq-nemp.smt2
new file mode 100644
index 000000000..4eaee062f
--- /dev/null
+++ b/test/regress/regress0/seq/seq-nemp.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_SLIA)
+(set-info :status sat)
+(declare-fun x () (Seq Int))
+(assert (not (= x (as seq.empty (Seq Int)))))
+(assert (= (seq.len x) 16))
+(check-sat)
diff --git a/test/regress/regress0/seq/seq-rewrites.smt2 b/test/regress/regress0/seq/seq-rewrites.smt2
new file mode 100644
index 000000000..a8bd7c1f2
--- /dev/null
+++ b/test/regress/regress0/seq/seq-rewrites.smt2
@@ -0,0 +1,44 @@
+(set-logic QF_UFSLIA)
+(set-info :status unsat)
+(declare-fun x () (Seq Int))
+(declare-fun y () (Seq Int))
+(declare-fun z () Int)
+
+(assert 
+(or
+
+(not (=
+(seq.replace (seq.++ (seq.unit 0) x) (seq.unit 1) (seq.unit 2))
+(seq.++ (seq.unit 0) (seq.replace x (seq.unit 1) (seq.unit 2)))
+))
+
+(not (=
+(seq.at (seq.++ x (seq.unit 14)) (seq.len x))
+(seq.unit 14)
+))
+
+(not (=
+(seq.at x z)
+(seq.extract x z 1)
+))
+
+(not (=
+(seq.contains (seq.++ x y) y)
+true
+))
+
+(not (=
+(seq.prefixof (seq.unit z) (seq.unit 4))
+(seq.suffixof (seq.unit z) (seq.unit 4))
+))
+
+(not (=
+(seq.rev (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3)))
+(seq.++ (seq.unit 3) (seq.unit 2) (seq.unit 1))
+))
+
+))
+
+
+
+(check-sat)