diff --git a/non-incremental/QF_S/20240318-omark/cloud-service-query-1.smt2 b/non-incremental/QF_S/20240318-omark/cloud-service-query-1.smt2
new file mode 100644
index 000000000..90d988cc5
--- /dev/null
+++ b/non-incremental/QF_S/20240318-omark/cloud-service-query-1.smt2
@@ -0,0 +1,42 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Query for Cloud Services
+Target solver: OSTRICH
+Simple word equation with regular constraints.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status sat)
+
+(declare-const V31 String)
+(declare-const V32 String)
+(declare-const V16 String)
+(declare-const V29 String)
+(declare-const V30 String)
+(declare-const V17 String)
+(declare-const k!8 String)
+(declare-const k!7 String)
+(declare-const k!3 String)
+(declare-const V33 String)
+(declare-const V34 String)
+(declare-const V35 String)
+(declare-const V3 String)
+(declare-const V36 String)
+(declare-const V37 String)
+(declare-const V1 String)
+
+(assert  (= (str.++ V31 "@" V32) (str.++ V16 V29 ":" V30 V17)))
+
+(assert  (= (str.++ V29 ":" V30) (str.++ k!8 "G" k!7)))
+
+(assert (= (str.++ V33 "/" V34) (str.++ V1 V31 "@" V32 V3)))
+
+(assert  (= (str.++ V36 "://" V37) (str.++ V33 "/" V34 k!3)))
+
+(assert  (= (str.++ "mongodb://" V35) (str.++ V33 "/" V34 k!3)))
+
+(check-sat)
+(exit)
diff --git a/non-incremental/QF_S/20240318-omark/cloud-service-query-2.smt2 b/non-incremental/QF_S/20240318-omark/cloud-service-query-2.smt2
new file mode 100644
index 000000000..91ed0b492
--- /dev/null
+++ b/non-incremental/QF_S/20240318-omark/cloud-service-query-2.smt2
@@ -0,0 +1,45 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Query for Cloud Services
+Target solver: OSTRICH
+Simple word equation with regular constraints.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unsat)
+
+(declare-const V31 String)
+(declare-const V32 String)
+(declare-const V16 String)
+(declare-const V29 String)
+(declare-const V30 String)
+(declare-const V17 String)
+(declare-const k!8 String)
+(declare-const k!7 String)
+(declare-const k!3 String)
+(declare-const V33 String)
+(declare-const V34 String)
+(declare-const V35 String)
+(declare-const V3 String)
+(declare-const V36 String)
+(declare-const V37 String)
+(declare-const V1 String)
+
+(assert  (= (str.++ V31 "@" V32) (str.++ V16 V29 ":" V30 V17)))
+
+(assert  (= (str.++ V29 ":" V30) (str.++ k!8 "G" k!7)))
+
+(assert (= (str.++ V33 "/" V34) (str.++ V1 V31 "@" V32 V3)))
+
+(assert  (= (str.++ V36 "://" V37) (str.++ V33 "/" V34 k!3)))
+
+(assert  (= (str.++ "mongodb://" V35) (str.++ V33 "/" V34 k!3)))
+
+(assert (str.in_re V31 (re.* (str.to_re "a"))))
+(assert (str.in_re V32 (re.* (str.to_re "b"))))
+
+(check-sat)
+(exit)
diff --git a/non-incremental/QF_S/20240318-omark/cyclic-xy.smt2 b/non-incremental/QF_S/20240318-omark/cyclic-xy.smt2
new file mode 100644
index 000000000..c811ab6ce
--- /dev/null
+++ b/non-incremental/QF_S/20240318-omark/cyclic-xy.smt2
@@ -0,0 +1,22 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Cyclic Word equations
+Target solver: OSTRICH
+Simple cyclic word equation with regular constraints.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unsat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+
+(assert (= (str.++ y x) (str.++ x y)))
+(assert (str.in_re x (re.union (str.to_re "a") (str.to_re "b"))))
+(assert (str.in_re y (re.union (str.to_re "bab") (str.to_re "aba"))))
+
+(check-sat)
+(exit)
diff --git a/non-incremental/QF_S/20240318-omark/lyndon-schuetzenberg-1.smt2 b/non-incremental/QF_S/20240318-omark/lyndon-schuetzenberg-1.smt2
new file mode 100644
index 000000000..031d3acbc
--- /dev/null
+++ b/non-incremental/QF_S/20240318-omark/lyndon-schuetzenberg-1.smt2
@@ -0,0 +1,26 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Instance of Lyndon-Schuetzenberger theorem
+Target solver: OSTRICH
+This benchmark is based on the Lyndon and Schützenberger theorem on word equations.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-fun X () String)
+(declare-fun A () String)
+(declare-fun B () String)
+(declare-fun C () String)
+(declare-fun D () String)
+(declare-fun E () String)
+
+(assert (= X (str.++ A B C)))
+(assert (= (str.++ X X) (str.++ A A B B C C)))
+(assert (= (str.++ X X X) (str.++ A A A B B B C C C)))
+(assert (str.in_re C (re.++(str.to_re "b") re.all)))
+(assert (str.in_re B (re.++(str.to_re "a") re.all)))
+(check-sat)
+(exit)
diff --git a/non-incremental/QF_S/20240318-omark/lyndon-schuetzenberg-2.smt2 b/non-incremental/QF_S/20240318-omark/lyndon-schuetzenberg-2.smt2
new file mode 100644
index 000000000..c0a15e62c
--- /dev/null
+++ b/non-incremental/QF_S/20240318-omark/lyndon-schuetzenberg-2.smt2
@@ -0,0 +1,27 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Instance of Lyndon-Schuetzenberger theorem
+Target solver: OSTRICH
+This benchmark is based on the Lyndon and Schützenberger theorem on word equations.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-fun X () String)
+(declare-fun A () String)
+(declare-fun B () String)
+(declare-fun C () String)
+(declare-fun D () String)
+(declare-fun E () String)
+
+(assert (= X (str.++ A B C)))
+(assert (= (str.++ X X) (str.++ A A B B C C)))
+(assert (= (str.++ X X X) (str.++ A A A B B B C C C)))
+(assert (str.in_re B (re.+ (str.to_re "b"))))
+(assert (str.in_re A (re.+ (str.to_re "a"))))
+(check-sat)
+(exit)
+
diff --git a/non-incremental/QF_S/20240318-omark/lyndon-schuetzenberg-3.smt2 b/non-incremental/QF_S/20240318-omark/lyndon-schuetzenberg-3.smt2
new file mode 100644
index 000000000..9072651a9
--- /dev/null
+++ b/non-incremental/QF_S/20240318-omark/lyndon-schuetzenberg-3.smt2
@@ -0,0 +1,27 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Instance of Lyndon-Schuetzenberger theorem
+Target solver: OSTRICH
+This benchmark is based on the Lyndon and Schützenberger theorem on word equations.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-fun X () String)
+(declare-fun A () String)
+(declare-fun B () String)
+(declare-fun C () String)
+(declare-fun D () String)
+(declare-fun E () String)
+
+(assert (= X (str.++ A B C)))
+(assert (= C (str.++ "b" D)))
+(assert (= B (str.++ "a" E)))
+(assert (= (str.++ X X) (str.++ A A B B C C)))
+(assert (= (str.++ X X X) (str.++ A A A B B B C C C)))
+
+(check-sat)
+(exit)
diff --git a/non-incremental/QF_S/20240318-omark/noodles-unsat-10.smt2 b/non-incremental/QF_S/20240318-omark/noodles-unsat-10.smt2
new file mode 100644
index 000000000..c1fe2b12d
--- /dev/null
+++ b/non-incremental/QF_S/20240318-omark/noodles-unsat-10.smt2
@@ -0,0 +1,22 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Word equations + Regular Constraints
+Target solver: OSTRICH
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unknown)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= (str.++ "2" y x) (str.++ x x "2")))
+(assert (str.in_re x (re.++(str.to_re "2") (re.union (re.* (str.to_re "1"))(re.* (str.to_re "2"))))))
+(assert (str.in_re y (re.++(str.to_re "2")(re.union (re.* (str.to_re "1"))(re.* (str.to_re "2"))))))
+
+(check-sat)
+(exit)
diff --git a/non-incremental/QF_S/20240318-omark/noodles-unsat-2.smt2 b/non-incremental/QF_S/20240318-omark/noodles-unsat-2.smt2
new file mode 100644
index 000000000..caf906ef7
--- /dev/null
+++ b/non-incremental/QF_S/20240318-omark/noodles-unsat-2.smt2
@@ -0,0 +1,24 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Word equations + Regular Constraints
+Target solver: OSTRICH
+This benchmark is a derivation from the introduction example in the paper "Word Equations in Synergy with Regular Constraints".
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unsat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= (str.++ z y x) (str.++ x z x z)))
+(assert (str.in_re x (re.* (str.to_re "1"))))
+(assert (str.in_re y (re.++ (re.+ (str.to_re "1"))  (re.+ (str.to_re "2")) )))
+(assert (str.in_re z (re.* (str.to_re "2"))))
+
+(check-sat)
+(exit)
diff --git a/non-incremental/QF_S/20240318-omark/noodles-unsat-3.smt2 b/non-incremental/QF_S/20240318-omark/noodles-unsat-3.smt2
new file mode 100644
index 000000000..3fb39d193
--- /dev/null
+++ b/non-incremental/QF_S/20240318-omark/noodles-unsat-3.smt2
@@ -0,0 +1,24 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Word equations + Regular Constraints
+Target solver: OSTRICH
+This benchmark is a derivation from the introduction example in the paper "Word Equations in Synergy with Regular Constraints".
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unsat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= (str.++ "1111" z "1" y x "21111") (str.++ "11" x x "111" z)))
+(assert (str.in_re x (re.++ (re.+ (str.to_re "1"))  (re.+ (str.to_re "2")) )))
+(assert (str.in_re y (re.++ (re.+ (str.to_re "1"))  (re.* (str.to_re "2")) )))
+(assert (str.in_re z (re.++ (re.+ (str.to_re "2"))  (re.* (str.to_re "1")) )))
+
+(check-sat)
+(exit)
diff --git a/non-incremental/QF_S/20240318-omark/noodles-unsat-4.smt2 b/non-incremental/QF_S/20240318-omark/noodles-unsat-4.smt2
new file mode 100644
index 000000000..6dd1ec1f4
--- /dev/null
+++ b/non-incremental/QF_S/20240318-omark/noodles-unsat-4.smt2
@@ -0,0 +1,24 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Word equations + Regular Constraints
+Target solver: OSTRICH
+This benchmark is a derivation from the introduction example in the paper "Word Equations in Synergy with Regular Constraints".
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unsat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= (str.++ z y x) (str.++ x x z)))
+(assert (str.in_re x (re.+ (str.to_re "1111"))))
+(assert (str.in_re y (str.to_re "11")))
+(assert (str.in_re z (re.+ (str.to_re "111"))))
+
+(check-sat)
+(exit)
diff --git a/non-incremental/QF_S/20240318-omark/noodles-unsat-5.smt2 b/non-incremental/QF_S/20240318-omark/noodles-unsat-5.smt2
new file mode 100644
index 000000000..72290f2fb
--- /dev/null
+++ b/non-incremental/QF_S/20240318-omark/noodles-unsat-5.smt2
@@ -0,0 +1,24 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Word equations + Regular Constraints
+Target solver: OSTRICH
+This benchmark is a derivation from the introduction example in the paper "Word Equations in Synergy with Regular Constraints".
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unsat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= (str.++ z y x) (str.++ x x z)))
+(assert (str.in_re x (re.++(str.to_re "2") re.all)))
+(assert (str.in_re y (re.++(str.to_re "1") re.all)))
+(assert (str.in_re z (re.++(str.to_re "2") re.all)))
+
+(check-sat)
+(exit)
diff --git a/non-incremental/QF_S/20240318-omark/noodles-unsat-6.smt2 b/non-incremental/QF_S/20240318-omark/noodles-unsat-6.smt2
new file mode 100644
index 000000000..f2045c111
--- /dev/null
+++ b/non-incremental/QF_S/20240318-omark/noodles-unsat-6.smt2
@@ -0,0 +1,24 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Word equations + Regular Constraints
+Target solver: OSTRICH
+This benchmark is a derivation from the introduction example in the paper "Word Equations in Synergy with Regular Constraints".
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unknown)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= (str.++ z y x) (str.++ x x z)))
+(assert (str.in_re x (re.++(str.to_re "2") (re.union (str.to_re "1")(str.to_re "2")))))
+(assert (str.in_re y (re.++(str.to_re "1") re.all)))
+(assert (str.in_re z (re.++(str.to_re "2") re.all)))
+
+(check-sat)
+(exit)
diff --git a/non-incremental/QF_S/20240318-omark/noodles-unsat-7.smt2 b/non-incremental/QF_S/20240318-omark/noodles-unsat-7.smt2
new file mode 100644
index 000000000..471913d16
--- /dev/null
+++ b/non-incremental/QF_S/20240318-omark/noodles-unsat-7.smt2
@@ -0,0 +1,24 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Word equations + Regular Constraints
+Target solver: OSTRICH
+This benchmark is a derivation from the introduction example in the paper "Word Equations in Synergy with Regular Constraints".
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unknown)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= (str.++ z y x) (str.++ x x z)))
+(assert (str.in_re x (re.++(str.to_re "2") re.all)))
+(assert (str.in_re y (re.++(str.to_re "1") re.all)))
+(assert (str.in_re z (str.to_re "2")))
+
+(check-sat)
+(exit)
diff --git a/non-incremental/QF_S/20240318-omark/noodles-unsat-8.smt2 b/non-incremental/QF_S/20240318-omark/noodles-unsat-8.smt2
new file mode 100644
index 000000000..8964ae3b3
--- /dev/null
+++ b/non-incremental/QF_S/20240318-omark/noodles-unsat-8.smt2
@@ -0,0 +1,24 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Word equations + Regular Constraints
+Target solver: OSTRICH
+This benchmark is a derivation from the introduction example in the paper "Word Equations in Synergy with Regular Constraints".
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unknown)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= (str.++ z y x) (str.++ x x z)))
+(assert (str.in_re x (re.++(str.to_re "2") (re.union (re.* (str.to_re "1"))(re.* (str.to_re "2"))))))
+(assert (str.in_re y (re.++(str.to_re "1") (re.union (re.* (str.to_re "1"))(re.* (str.to_re "2"))))))
+(assert (str.in_re z (re.++(str.to_re "2") re.all)))
+
+(check-sat)
+(exit)
diff --git a/non-incremental/QF_S/20240318-omark/noodles-unsat-9.smt2 b/non-incremental/QF_S/20240318-omark/noodles-unsat-9.smt2
new file mode 100644
index 000000000..ae7757cd5
--- /dev/null
+++ b/non-incremental/QF_S/20240318-omark/noodles-unsat-9.smt2
@@ -0,0 +1,23 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Word equations + Regular Constraints
+Target solver: OSTRICH
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unknown)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= (str.++ z y x) (str.++ x x z)))
+(assert (str.in_re x (re.++(str.to_re "2") (re.* (re.union (str.to_re "1")(re.* (str.to_re "2")))))))
+(assert (str.in_re y (re.++(str.to_re "1") (re.* (re.union (str.to_re "1")(re.* (str.to_re "2")))))))
+(assert (str.in_re z (re.++(str.to_re "2") (re.* (re.union (str.to_re "1")(re.* (str.to_re "2")))))))
+
+(check-sat)
+(exit)
diff --git a/non-incremental/QF_S/20240318-omark/noodles-unsat.smt2 b/non-incremental/QF_S/20240318-omark/noodles-unsat.smt2
new file mode 100644
index 000000000..00224bf85
--- /dev/null
+++ b/non-incremental/QF_S/20240318-omark/noodles-unsat.smt2
@@ -0,0 +1,24 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Word equations + Regular Constraints
+Target solver: OSTRICH
+This benchmark is a derivation from the introduction example in the paper "Word Equations in Synergy with Regular Constraints".
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unsat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= (str.++ z y x) (str.++ x x z)))
+(assert (str.in_re x (re.* (str.to_re "1"))))
+(assert (str.in_re y (re.++ (re.+ (str.to_re "1"))  (re.+ (str.to_re "2")) )))
+(assert (str.in_re z (re.* (str.to_re "2"))))
+
+(check-sat)
+(exit)
diff --git a/non-incremental/QF_S/20240318-omark/parikh.smt2 b/non-incremental/QF_S/20240318-omark/parikh.smt2
new file mode 100644
index 000000000..f7e8153ca
--- /dev/null
+++ b/non-incremental/QF_S/20240318-omark/parikh.smt2
@@ -0,0 +1,17 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Cyclic Word equation
+Target solver: OSTRICH
+Simple cyclic word equation.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unsat)
+
+(declare-fun x () String)
+(assert (= (str.++ x x "b" x)(str.++ x "a" x x)))
+(check-sat)
+(exit)