4 different benchmark sets focused around str.replace_all

non-incremental/QF_S/20250403-pcp-string/pcp-3-3-random/pcp_instance_0.smt2

@@ -0,0 +1,53 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2025-04-03
+Application: Evaluation of String Solvers on PCP
+Target solver: cvc5, Z3, OSTRICH
+Time limit: 60.0
+Benchmarks encoding PCP[3,3] on randomly generated strings with exactly length 3.
+Most benchmarks expected to be unsat.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unknown)
+
+(declare-fun TopStr () String)
+(declare-fun BottomStr () String)
+
+(declare-fun Top_0 () String)
+(declare-fun Bottom_0 () String)
+(assert (= Top_0 "001"))
+(assert (= Bottom_0 "010"))
+(declare-fun Top_1 () String)
+(declare-fun Bottom_1 () String)
+(assert (= Top_1 "010"))
+(assert (= Bottom_1 "111"))
+(declare-fun Top_2 () String)
+(declare-fun Bottom_2 () String)
+(assert (= Top_2 "000"))
+(assert (= Bottom_2 "011"))
+(declare-fun replace () String)
+(assert (str.in_re replace (re.+ (re.union (str.to_re "2") (str.to_re "3") (str.to_re "4")))))
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun x_0 () String)
+(declare-fun y_0 () String)
+(declare-fun x_1 () String)
+(declare-fun y_1 () String)
+(declare-fun x_2 () String)
+(declare-fun y_2 () String)
+(assert (= x_1 (str.replace_all x_0 "2" Top_0)))
+(assert (= x_2 (str.replace_all x_1 "3" Top_1)))
+(assert (= x (str.replace_all x_2 "4" Top_2)))
+(assert (= y_1 (str.replace_all y_0 "2" Bottom_0)))
+(assert (= y_2 (str.replace_all y_1 "3" Bottom_1)))
+(assert (= y (str.replace_all y_2 "4" Bottom_2)))
+(assert (= x_0 replace))
+(assert (= y_0 replace))
+
+(assert (= x y))
+(check-sat)
+(exit)

non-incremental/QF_S/20250403-pcp-string/pcp-3-3-random/pcp_instance_1.smt2

@@ -0,0 +1,53 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2025-04-03
+Application: Evaluation of String Solvers on PCP
+Target solver: cvc5, Z3, OSTRICH
+Time limit: 60.0
+Benchmarks encoding PCP[3,3] on randomly generated strings with exactly length 3.
+Most benchmarks expected to be unsat.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unknown)
+
+(declare-fun TopStr () String)
+(declare-fun BottomStr () String)
+
+(declare-fun Top_0 () String)
+(declare-fun Bottom_0 () String)
+(assert (= Top_0 "110"))
+(assert (= Bottom_0 "101"))
+(declare-fun Top_1 () String)
+(declare-fun Bottom_1 () String)
+(assert (= Top_1 "101"))
+(assert (= Bottom_1 "011"))
+(declare-fun Top_2 () String)
+(declare-fun Bottom_2 () String)
+(assert (= Top_2 "010"))
+(assert (= Bottom_2 "000"))
+(declare-fun replace () String)
+(assert (str.in_re replace (re.+ (re.union (str.to_re "2") (str.to_re "3") (str.to_re "4")))))
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun x_0 () String)
+(declare-fun y_0 () String)
+(declare-fun x_1 () String)
+(declare-fun y_1 () String)
+(declare-fun x_2 () String)
+(declare-fun y_2 () String)
+(assert (= x_1 (str.replace_all x_0 "2" Top_0)))
+(assert (= x_2 (str.replace_all x_1 "3" Top_1)))
+(assert (= x (str.replace_all x_2 "4" Top_2)))
+(assert (= y_1 (str.replace_all y_0 "2" Bottom_0)))
+(assert (= y_2 (str.replace_all y_1 "3" Bottom_1)))
+(assert (= y (str.replace_all y_2 "4" Bottom_2)))
+(assert (= x_0 replace))
+(assert (= y_0 replace))
+
+(assert (= x y))
+(check-sat)
+(exit)

non-incremental/QF_S/20250403-pcp-string/pcp-3-3-random/pcp_instance_10.smt2

@@ -0,0 +1,53 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2025-04-03
+Application: Evaluation of String Solvers on PCP
+Target solver: cvc5, Z3, OSTRICH
+Time limit: 60.0
+Benchmarks encoding PCP[3,3] on randomly generated strings with exactly length 3.
+Most benchmarks expected to be unsat.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unknown)
+
+(declare-fun TopStr () String)
+(declare-fun BottomStr () String)
+
+(declare-fun Top_0 () String)
+(declare-fun Bottom_0 () String)
+(assert (= Top_0 "101"))
+(assert (= Bottom_0 "100"))
+(declare-fun Top_1 () String)
+(declare-fun Bottom_1 () String)
+(assert (= Top_1 "111"))
+(assert (= Bottom_1 "101"))
+(declare-fun Top_2 () String)
+(declare-fun Bottom_2 () String)
+(assert (= Top_2 "011"))
+(assert (= Bottom_2 "101"))
+(declare-fun replace () String)
+(assert (str.in_re replace (re.+ (re.union (str.to_re "2") (str.to_re "3") (str.to_re "4")))))
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun x_0 () String)
+(declare-fun y_0 () String)
+(declare-fun x_1 () String)
+(declare-fun y_1 () String)
+(declare-fun x_2 () String)
+(declare-fun y_2 () String)
+(assert (= x_1 (str.replace_all x_0 "2" Top_0)))
+(assert (= x_2 (str.replace_all x_1 "3" Top_1)))
+(assert (= x (str.replace_all x_2 "4" Top_2)))
+(assert (= y_1 (str.replace_all y_0 "2" Bottom_0)))
+(assert (= y_2 (str.replace_all y_1 "3" Bottom_1)))
+(assert (= y (str.replace_all y_2 "4" Bottom_2)))
+(assert (= x_0 replace))
+(assert (= y_0 replace))
+
+(assert (= x y))
+(check-sat)
+(exit)

non-incremental/QF_S/20250403-pcp-string/pcp-3-3-random/pcp_instance_100.smt2

@@ -0,0 +1,53 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2025-04-03
+Application: Evaluation of String Solvers on PCP
+Target solver: cvc5, Z3, OSTRICH
+Time limit: 60.0
+Benchmarks encoding PCP[3,3] on randomly generated strings with exactly length 3.
+Most benchmarks expected to be unsat.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unknown)
+
+(declare-fun TopStr () String)
+(declare-fun BottomStr () String)
+
+(declare-fun Top_0 () String)
+(declare-fun Bottom_0 () String)
+(assert (= Top_0 "010"))
+(assert (= Bottom_0 "111"))
+(declare-fun Top_1 () String)
+(declare-fun Bottom_1 () String)
+(assert (= Top_1 "010"))
+(assert (= Bottom_1 "000"))
+(declare-fun Top_2 () String)
+(declare-fun Bottom_2 () String)
+(assert (= Top_2 "010"))
+(assert (= Bottom_2 "011"))
+(declare-fun replace () String)
+(assert (str.in_re replace (re.+ (re.union (str.to_re "2") (str.to_re "3") (str.to_re "4")))))
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun x_0 () String)
+(declare-fun y_0 () String)
+(declare-fun x_1 () String)
+(declare-fun y_1 () String)
+(declare-fun x_2 () String)
+(declare-fun y_2 () String)
+(assert (= x_1 (str.replace_all x_0 "2" Top_0)))
+(assert (= x_2 (str.replace_all x_1 "3" Top_1)))
+(assert (= x (str.replace_all x_2 "4" Top_2)))
+(assert (= y_1 (str.replace_all y_0 "2" Bottom_0)))
+(assert (= y_2 (str.replace_all y_1 "3" Bottom_1)))
+(assert (= y (str.replace_all y_2 "4" Bottom_2)))
+(assert (= x_0 replace))
+(assert (= y_0 replace))
+
+(assert (= x y))
+(check-sat)
+(exit)

non-incremental/QF_S/20250403-pcp-string/pcp-3-3-random/pcp_instance_101.smt2

@@ -0,0 +1,53 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2025-04-03
+Application: Evaluation of String Solvers on PCP
+Target solver: cvc5, Z3, OSTRICH
+Time limit: 60.0
+Benchmarks encoding PCP[3,3] on randomly generated strings with exactly length 3.
+Most benchmarks expected to be unsat.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unknown)
+
+(declare-fun TopStr () String)
+(declare-fun BottomStr () String)
+
+(declare-fun Top_0 () String)
+(declare-fun Bottom_0 () String)
+(assert (= Top_0 "111"))
+(assert (= Bottom_0 "100"))
+(declare-fun Top_1 () String)
+(declare-fun Bottom_1 () String)
+(assert (= Top_1 "101"))
+(assert (= Bottom_1 "000"))
+(declare-fun Top_2 () String)
+(declare-fun Bottom_2 () String)
+(assert (= Top_2 "101"))
+(assert (= Bottom_2 "001"))
+(declare-fun replace () String)
+(assert (str.in_re replace (re.+ (re.union (str.to_re "2") (str.to_re "3") (str.to_re "4")))))
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun x_0 () String)
+(declare-fun y_0 () String)
+(declare-fun x_1 () String)
+(declare-fun y_1 () String)
+(declare-fun x_2 () String)
+(declare-fun y_2 () String)
+(assert (= x_1 (str.replace_all x_0 "2" Top_0)))
+(assert (= x_2 (str.replace_all x_1 "3" Top_1)))
+(assert (= x (str.replace_all x_2 "4" Top_2)))
+(assert (= y_1 (str.replace_all y_0 "2" Bottom_0)))
+(assert (= y_2 (str.replace_all y_1 "3" Bottom_1)))
+(assert (= y (str.replace_all y_2 "4" Bottom_2)))
+(assert (= x_0 replace))
+(assert (= y_0 replace))
+
+(assert (= x y))
+(check-sat)
+(exit)

non-incremental/QF_S/20250403-pcp-string/pcp-3-3-random/pcp_instance_102.smt2

@@ -0,0 +1,53 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2025-04-03
+Application: Evaluation of String Solvers on PCP
+Target solver: cvc5, Z3, OSTRICH
+Time limit: 60.0
+Benchmarks encoding PCP[3,3] on randomly generated strings with exactly length 3.
+Most benchmarks expected to be unsat.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unknown)
+
+(declare-fun TopStr () String)
+(declare-fun BottomStr () String)
+
+(declare-fun Top_0 () String)
+(declare-fun Bottom_0 () String)
+(assert (= Top_0 "000"))
+(assert (= Bottom_0 "100"))
+(declare-fun Top_1 () String)
+(declare-fun Bottom_1 () String)
+(assert (= Top_1 "011"))
+(assert (= Bottom_1 "010"))
+(declare-fun Top_2 () String)
+(declare-fun Bottom_2 () String)
+(assert (= Top_2 "001"))
+(assert (= Bottom_2 "010"))
+(declare-fun replace () String)
+(assert (str.in_re replace (re.+ (re.union (str.to_re "2") (str.to_re "3") (str.to_re "4")))))
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun x_0 () String)
+(declare-fun y_0 () String)
+(declare-fun x_1 () String)
+(declare-fun y_1 () String)
+(declare-fun x_2 () String)
+(declare-fun y_2 () String)
+(assert (= x_1 (str.replace_all x_0 "2" Top_0)))
+(assert (= x_2 (str.replace_all x_1 "3" Top_1)))
+(assert (= x (str.replace_all x_2 "4" Top_2)))
+(assert (= y_1 (str.replace_all y_0 "2" Bottom_0)))
+(assert (= y_2 (str.replace_all y_1 "3" Bottom_1)))
+(assert (= y (str.replace_all y_2 "4" Bottom_2)))
+(assert (= x_0 replace))
+(assert (= y_0 replace))
+
+(assert (= x y))
+(check-sat)
+(exit)

non-incremental/QF_S/20250403-pcp-string/pcp-3-3-random/pcp_instance_103.smt2

@@ -0,0 +1,53 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2025-04-03
+Application: Evaluation of String Solvers on PCP
+Target solver: cvc5, Z3, OSTRICH
+Time limit: 60.0
+Benchmarks encoding PCP[3,3] on randomly generated strings with exactly length 3.
+Most benchmarks expected to be unsat.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unknown)
+
+(declare-fun TopStr () String)
+(declare-fun BottomStr () String)
+
+(declare-fun Top_0 () String)
+(declare-fun Bottom_0 () String)
+(assert (= Top_0 "011"))
+(assert (= Bottom_0 "111"))
+(declare-fun Top_1 () String)
+(declare-fun Bottom_1 () String)
+(assert (= Top_1 "011"))
+(assert (= Bottom_1 "111"))
+(declare-fun Top_2 () String)
+(declare-fun Bottom_2 () String)
+(assert (= Top_2 "101"))
+(assert (= Bottom_2 "110"))
+(declare-fun replace () String)
+(assert (str.in_re replace (re.+ (re.union (str.to_re "2") (str.to_re "3") (str.to_re "4")))))
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun x_0 () String)
+(declare-fun y_0 () String)
+(declare-fun x_1 () String)
+(declare-fun y_1 () String)
+(declare-fun x_2 () String)
+(declare-fun y_2 () String)
+(assert (= x_1 (str.replace_all x_0 "2" Top_0)))
+(assert (= x_2 (str.replace_all x_1 "3" Top_1)))
+(assert (= x (str.replace_all x_2 "4" Top_2)))
+(assert (= y_1 (str.replace_all y_0 "2" Bottom_0)))
+(assert (= y_2 (str.replace_all y_1 "3" Bottom_1)))
+(assert (= y (str.replace_all y_2 "4" Bottom_2)))
+(assert (= x_0 replace))
+(assert (= y_0 replace))
+
+(assert (= x y))
+(check-sat)
+(exit)