From 243ebe0660d2e3087cb11474a18c2942e830d6c1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 6 Jun 2026 15:31:19 -0700 Subject: [PATCH] remove local copies of benchmarks Signed-off-by: Nikolaj Bjorner --- benchmarks/instance08965.smt2 | 23 ----------------------- benchmarks/instance09159.smt2 | 23 ----------------------- benchmarks/instance11213.smt2 | 22 ---------------------- benchmarks/instance11705.smt2 | 23 ----------------------- benchmarks/instance11745.smt2 | 21 --------------------- benchmarks/instance11856.smt2 | 21 --------------------- benchmarks/instance12204.smt2 | 22 ---------------------- benchmarks/instance12488.smt2 | 22 ---------------------- benchmarks/instance12671.smt2 | 21 --------------------- benchmarks/instance12768.smt2 | 22 ---------------------- benchmarks/instance12833.smt2 | 22 ---------------------- benchmarks/instance13062.smt2 | 23 ----------------------- benchmarks/instance13106.smt2 | 23 ----------------------- benchmarks/instance13975.smt2 | 22 ---------------------- benchmarks/instance14260.smt2 | 23 ----------------------- benchmarks/instance14326.smt2 | 21 --------------------- benchmarks/instance14382.smt2 | 21 --------------------- 17 files changed, 375 deletions(-) delete mode 100644 benchmarks/instance08965.smt2 delete mode 100644 benchmarks/instance09159.smt2 delete mode 100644 benchmarks/instance11213.smt2 delete mode 100644 benchmarks/instance11705.smt2 delete mode 100644 benchmarks/instance11745.smt2 delete mode 100644 benchmarks/instance11856.smt2 delete mode 100644 benchmarks/instance12204.smt2 delete mode 100644 benchmarks/instance12488.smt2 delete mode 100644 benchmarks/instance12671.smt2 delete mode 100644 benchmarks/instance12768.smt2 delete mode 100644 benchmarks/instance12833.smt2 delete mode 100644 benchmarks/instance13062.smt2 delete mode 100644 benchmarks/instance13106.smt2 delete mode 100644 benchmarks/instance13975.smt2 delete mode 100644 benchmarks/instance14260.smt2 delete mode 100644 benchmarks/instance14326.smt2 delete mode 100644 benchmarks/instance14382.smt2 diff --git a/benchmarks/instance08965.smt2 b/benchmarks/instance08965.smt2 deleted file mode 100644 index 4449c9d4e..000000000 --- a/benchmarks/instance08965.smt2 +++ /dev/null @@ -1,23 +0,0 @@ -(set-info :smt-lib-version 2.6) -(set-logic QF_S) -(set-info :source | -Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu -Generated on: 2020-10-01 -Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark -Application: Evaluate solvers on real-world regex queries -Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau -Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. -|) -(set-info :license "https://creativecommons.org/licenses/by/4.0/") -(set-info :category "industrial") -(set-info :status unsat) - -(declare-const X String) -(assert (str.in_re X (re.++ (str.to_re "qr/") (re.union (str.to_re "Alabama") (str.to_re "Alaska") (str.to_re "Arizona") (str.to_re "Arkansas") (str.to_re "California") (str.to_re "Colorado") (str.to_re "Connecticut") (str.to_re "Delaware") (str.to_re "Florida") (str.to_re "Georgia") (str.to_re "Hawaii") (str.to_re "Idaho") (str.to_re "Illinois") (str.to_re "Indiana") (str.to_re "Iowa") (str.to_re "Kansas") (str.to_re "Kentucky") (str.to_re "Louisiana") (str.to_re "Maine") (str.to_re "Maryland") (str.to_re "Massachusetts") (str.to_re "Michigan") (str.to_re "Minnesota") (str.to_re "Mississippi") (str.to_re "Missouri") (str.to_re "Montana") (str.to_re "Nebraska") (str.to_re "Nevada") (re.++ (str.to_re "New") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Hampshire")) (re.++ (str.to_re "New") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Jersey")) (re.++ (str.to_re "New") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Mexico")) (re.++ (str.to_re "New") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "York")) (re.++ (str.to_re "North") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Carolina")) (re.++ (str.to_re "North") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Dakota")) (str.to_re "Ohio") (str.to_re "Oklahoma") (str.to_re "Oregon") (str.to_re "Pennsylvania") (re.++ (str.to_re "Rhode") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Island")) (re.++ (str.to_re "South") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Carolina")) (re.++ (str.to_re "South") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Dakota")) (str.to_re "Tennessee") (str.to_re "Texas") (str.to_re "Utah") (str.to_re "Vermont") (str.to_re "Virginia") (str.to_re "Washington") (re.++ (str.to_re "West") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Virginia")) (str.to_re "Wisconsin") (str.to_re "Wyoming")) (str.to_re "/\u{a}")))) -(assert (str.in_re X (re.++ (str.to_re "6") ((_ re.loop 7 7) (re.range "0" "9")) (str.to_re "\u{a}")))) -(assert (str.in_re X (re.++ (str.to_re "/Referer:") (re.+ (re.union (str.to_re "\u{d}") (str.to_re "\u{a}"))) (str.to_re "/.html\u{d}/Hsm\u{a}") ((_ re.loop 32 32) (re.union (str.to_re "_") (re.range "0" "9") (re.range "A" "Z") (re.range "a" "z") (str.to_re "_"))) (re.* (re.union (str.to_re "_") (re.range "0" "9") (re.range "A" "Z") (re.range "a" "z") (str.to_re "_")))))) -(assert (str.in_re X (re.++ (str.to_re "Wareztv.seekmo.com") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Keylogging\u{13}TRUSTYFILES.COM\u{a}")))) -(assert (not (str.in_re X (re.++ (str.to_re "Flooded") (re.+ (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "Host:") (re.+ (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "AppName/GRSI|Server|\u{13}Host:origin=sidefindHost:User-Agent:\u{a}"))))) -(check-sat) - -(exit) diff --git a/benchmarks/instance09159.smt2 b/benchmarks/instance09159.smt2 deleted file mode 100644 index 2d5e138d9..000000000 --- a/benchmarks/instance09159.smt2 +++ /dev/null @@ -1,23 +0,0 @@ -(set-info :smt-lib-version 2.6) -(set-logic QF_S) -(set-info :source | -Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu -Generated on: 2020-10-01 -Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark -Application: Evaluate solvers on real-world regex queries -Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau -Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. -|) -(set-info :license "https://creativecommons.org/licenses/by/4.0/") -(set-info :category "industrial") -(set-info :status sat) - -(declare-const X String) -(assert (not (str.in_re X (re.++ (str.to_re "__") (re.+ re.allchar) (str.to_re "__\u{a}"))))) -(assert (not (str.in_re X (re.++ (str.to_re "/.avi") (re.union (str.to_re "?") (str.to_re "\u{5c}") (str.to_re "/")) (str.to_re "/smiU\u{a}"))))) -(assert (not (str.in_re X (re.++ (str.to_re "User") (re.* re.allchar) (str.to_re "User-Agent:") (re.* re.allchar) (str.to_re "ResultATTENTION:riggiymd/wdhi.vhi\u{a}"))))) -(assert (str.in_re X (re.++ (re.union (re.++ (str.to_re "A") (re.union (str.to_re "BW") (str.to_re "FG") (str.to_re "GO") (str.to_re "IA") (re.++ (str.to_re "L") (re.union (str.to_re "A") (str.to_re "B"))) (re.++ (str.to_re "N") (re.union (str.to_re "D") (str.to_re "T"))) (re.++ (str.to_re "R") (re.union (str.to_re "E") (str.to_re "G") (str.to_re "M"))) (str.to_re "SM") (re.++ (str.to_re "T") (re.union (str.to_re "A") (str.to_re "F") (str.to_re "G"))) (re.++ (str.to_re "U") (re.union (str.to_re "S") (str.to_re "T"))) (str.to_re "ZE"))) (re.++ (str.to_re "B") (re.union (str.to_re "DI") (re.++ (str.to_re "E") (re.union (str.to_re "L") (str.to_re "N"))) (str.to_re "FA") (re.++ (str.to_re "G") (re.union (str.to_re "D") (str.to_re "R"))) (re.++ (str.to_re "H") (re.union (str.to_re "R") (str.to_re "S"))) (str.to_re "IH") (re.++ (str.to_re "L") (re.union (str.to_re "M") (str.to_re "R") (str.to_re "Z"))) (str.to_re "MU") (str.to_re "OL") (re.++ (str.to_re "R") (re.union (str.to_re "A") (str.to_re "B") (str.to_re "N"))) (str.to_re "TN") (str.to_re "VT") (str.to_re "WA"))) (re.++ (str.to_re "C") (re.union (re.++ (str.to_re "A") (re.union (str.to_re "F") (str.to_re "N"))) (str.to_re "CK") (re.++ (str.to_re "H") (re.union (str.to_re "E") (str.to_re "L") (str.to_re "N"))) (str.to_re "IV") (str.to_re "MR") (re.++ (str.to_re "O") (re.union (str.to_re "D") (str.to_re "G") (str.to_re "K") (str.to_re "L") (str.to_re "M"))) (str.to_re "PV") (str.to_re "RI") (str.to_re "UB") (str.to_re "XR") (re.++ (str.to_re "Y") (re.union (str.to_re "M") (str.to_re "P"))) (str.to_re "ZE"))) (re.++ (str.to_re "D") (re.union (str.to_re "EU") (str.to_re "JI") (str.to_re "MA") (str.to_re "NK") (str.to_re "OM") (str.to_re "ZA"))) (re.++ (str.to_re "E") (re.union (str.to_re "CU") (str.to_re "GY") (str.to_re "RI") (re.++ (str.to_re "S") (re.union (str.to_re "H") (str.to_re "P") (str.to_re "T"))) (str.to_re "TH"))) (re.++ (str.to_re "F") (re.union (str.to_re "IN") (str.to_re "JI") (str.to_re "LK") (re.++ (str.to_re "R") (re.union (str.to_re "A") (str.to_re "O"))) (str.to_re "SM"))) (re.++ (str.to_re "G") (re.union (str.to_re "AB") (str.to_re "BR") (str.to_re "EO") (str.to_re "GY") (str.to_re "HA") (re.++ (str.to_re "I") (re.union (str.to_re "B") (str.to_re "N"))) (str.to_re "LP") (str.to_re "MB") (str.to_re "NQ") (str.to_re "NB") (re.++ (str.to_re "R") (re.union (str.to_re "C") (str.to_re "D") (str.to_re "L"))) (str.to_re "TM") (re.++ (str.to_re "U") (re.union (str.to_re "F") (str.to_re "M") (str.to_re "Y"))))) (re.++ (str.to_re "H") (re.union (str.to_re "KG") (str.to_re "MD") (str.to_re "ND") (str.to_re "RV") (str.to_re "TI") (str.to_re "UN"))) (re.++ (str.to_re "I") (re.union (str.to_re "DN") (str.to_re "MN") (str.to_re "ND") (str.to_re "OT") (re.++ (str.to_re "R") (re.union (str.to_re "L") (str.to_re "N") (str.to_re "Q"))) (re.++ (str.to_re "S") (re.union (str.to_re "L") (str.to_re "R"))) (str.to_re "TA"))) (re.++ (str.to_re "J") (re.union (str.to_re "AM") (str.to_re "EY") (str.to_re "OR") (str.to_re "PN"))) (re.++ (str.to_re "K") (re.union (str.to_re "AZ") (str.to_re "EN") (str.to_re "GZ") (str.to_re "HM") (str.to_re "IR") (str.to_re "NA") (str.to_re "OR") (str.to_re "WT"))) (re.++ (str.to_re "L") (re.union (str.to_re "AO") (re.++ (str.to_re "B") (re.union (str.to_re "N") (str.to_re "R") (str.to_re "Y"))) (str.to_re "CA") (str.to_re "IE") (str.to_re "KA") (str.to_re "SO") (str.to_re "TU") (str.to_re "UX") (str.to_re "VA"))) (re.++ (str.to_re "M") (re.union (re.++ (str.to_re "A") (re.union (str.to_re "C") (str.to_re "F") (str.to_re "R"))) (str.to_re "CO") (re.++ (str.to_re "D") (re.union (str.to_re "A") (str.to_re "G") (str.to_re "V"))) (str.to_re "EX") (str.to_re "HL") (str.to_re "KD") (re.++ (str.to_re "L") (re.union (str.to_re "I") (str.to_re "T"))) (str.to_re "MR") (re.++ (str.to_re "N") (re.union (str.to_re "E") (str.to_re "G") (str.to_re "P"))) (str.to_re "OZ") (str.to_re "RT") (str.to_re "SR") (str.to_re "TQ") (str.to_re "US") (str.to_re "WI") (re.++ (str.to_re "Y") (re.union (str.to_re "S") (str.to_re "T"))))) (re.++ (str.to_re "N") (re.union (str.to_re "AM") (str.to_re "CL") (str.to_re "ER") (str.to_re "FK") (str.to_re "GA") (re.++ (str.to_re "I") (re.union (str.to_re "C") (str.to_re "U"))) (str.to_re "LD") (str.to_re "OR") (str.to_re "PL") (str.to_re "RU") (str.to_re "ZL"))) (str.to_re "OMN") (re.++ (str.to_re "P") (re.union (re.++ (str.to_re "A") (re.union (str.to_re "K") (str.to_re "N"))) (str.to_re "CN") (str.to_re "ER") (str.to_re "HL") (str.to_re "LW") (str.to_re "NG") (str.to_re "OL") (re.++ (str.to_re "R") (re.union (str.to_re "I") (str.to_re "K") (str.to_re "T") (str.to_re "Y"))) (str.to_re "SE") (str.to_re "YF"))) (str.to_re "QAT") (re.++ (str.to_re "R") (re.union (str.to_re "EU") (str.to_re "OU") (str.to_re "US") (str.to_re "WA"))) (re.++ (str.to_re "S") (re.union (str.to_re "AU") (str.to_re "DN") (str.to_re "EN") (re.++ (str.to_re "G") (re.union (str.to_re "P") (str.to_re "S"))) (str.to_re "HN") (str.to_re "JM") (re.++ (str.to_re "L") (re.union (str.to_re "B") (str.to_re "E") (str.to_re "V"))) (str.to_re "MR") (str.to_re "OM") (str.to_re "PM") (str.to_re "RB") (str.to_re "TP") (str.to_re "UR") (re.++ (str.to_re "V") (re.union (str.to_re "K") (str.to_re "N"))) (re.++ (str.to_re "W") (re.union (str.to_re "E") (str.to_re "Z"))) (re.++ (str.to_re "Y") (re.union (str.to_re "C") (str.to_re "R"))))) (re.++ (str.to_re "T") (re.union (re.++ (str.to_re "C") (re.union (str.to_re "A") (str.to_re "D"))) (str.to_re "GO") (str.to_re "HA") (str.to_re "JK") (re.++ (str.to_re "K") (re.union (str.to_re "L") (str.to_re "M"))) (str.to_re "LS") (str.to_re "ON") (str.to_re "TO") (re.++ (str.to_re "U") (re.union (str.to_re "N") (str.to_re "R") (str.to_re "V"))) (str.to_re "WN") (str.to_re "ZA"))) (re.++ (str.to_re "U") (re.union (str.to_re "EN") (str.to_re "GA") (str.to_re "KR") (str.to_re "MI") (str.to_re "RY") (str.to_re "SA") (str.to_re "ZB"))) (re.++ (str.to_re "V") (re.union (str.to_re "AT") (str.to_re "CT") (str.to_re "GB") (str.to_re "IR") (str.to_re "NM") (str.to_re "UT"))) (re.++ (str.to_re "W") (re.union (str.to_re "LF") (str.to_re "SM"))) (str.to_re "YEM") (re.++ (str.to_re "Z") (re.union (str.to_re "AF") (str.to_re "MB") (str.to_re "WE")))) (str.to_re "\u{a}")))) -(assert (not (str.in_re X (re.++ (re.* (re.++ ((_ re.loop 2 2) (re.range "0" "9")) (str.to_re "-") ((_ re.loop 2 2) (re.range "0" "9")))) (str.to_re "\u{a}"))))) -(check-sat) - -(exit) diff --git a/benchmarks/instance11213.smt2 b/benchmarks/instance11213.smt2 deleted file mode 100644 index 0bdec4a17..000000000 --- a/benchmarks/instance11213.smt2 +++ /dev/null @@ -1,22 +0,0 @@ -(set-info :smt-lib-version 2.6) -(set-logic QF_S) -(set-info :source | -Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu -Generated on: 2020-10-01 -Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark -Application: Evaluate solvers on real-world regex queries -Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau -Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. -|) -(set-info :license "https://creativecommons.org/licenses/by/4.0/") -(set-info :category "industrial") -(set-info :status unsat) - -(declare-const X String) -(assert (not (str.in_re X (re.++ (str.to_re "//") ((_ re.loop 48 48) (re.union (str.to_re "-") (re.range "0" "9") (re.range "A" "Z") (re.range "a" "z") (str.to_re "_"))) (str.to_re "/U\u{a}"))))) -(assert (str.in_re X (re.++ (re.opt (re.++ (re.opt (str.to_re " ")) (re.opt (str.to_re "+")) (str.to_re "34"))) (re.union (re.++ (str.to_re "6") (re.union ((_ re.loop 8 8) (re.range "0" "9")) (re.++ ((_ re.loop 2 2) (re.range "0" "9")) (str.to_re " ") ((_ re.loop 6 6) (re.range "0" "9"))) (re.++ ((_ re.loop 2 2) (re.range "0" "9")) (str.to_re " ") ((_ re.loop 3 3) (re.range "0" "9")) (str.to_re " ") ((_ re.loop 3 3) (re.range "0" "9"))))) (re.++ (str.to_re "9") (re.union ((_ re.loop 8 8) (re.range "0" "9")) (re.++ ((_ re.loop 2 2) (re.range "0" "9")) (str.to_re " ") ((_ re.loop 6 6) (re.range "0" "9"))) (re.++ (re.range "1" "9") (str.to_re " ") ((_ re.loop 7 7) (re.range "0" "9"))) (re.++ ((_ re.loop 2 2) (re.range "0" "9")) (str.to_re " ") ((_ re.loop 3 3) (re.range "0" "9")) (str.to_re " ") ((_ re.loop 3 3) (re.range "0" "9"))) (re.++ ((_ re.loop 2 2) (re.range "0" "9")) (str.to_re " ") ((_ re.loop 2 2) (re.range "0" "9")) (str.to_re " ") ((_ re.loop 2 2) (re.range "0" "9")) (str.to_re " ") ((_ re.loop 2 2) (re.range "0" "9")))))) (str.to_re "\u{a}")))) -(assert (str.in_re X (re.++ (re.+ (re.union (re.range "a" "z") (re.range "A" "Z") (re.range "0" "9") (str.to_re ".") (str.to_re "-") (str.to_re "_") (str.to_re "'") (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "\u{a}")))) -(assert (str.in_re X (re.union (re.++ (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "general") (str.to_re "unicode") (str.to_re "roman") (str.to_re "slovak") (str.to_re "czech") (str.to_re "icelandic") (re.++ (re.union (str.to_re "latv") (str.to_re "pers")) (str.to_re "ian")) (re.++ (re.union (str.to_re "dan") (str.to_re "pol") (str.to_re "span") (str.to_re "swed") (str.to_re "turk")) (str.to_re "ish")) (str.to_re "spanish2") (re.++ (re.union (str.to_re "esto") (str.to_re "lithua") (str.to_re "roma") (str.to_re "slove")) (str.to_re "nian_ci"))) (str.to_re "u") (re.union (str.to_re "cs2") (str.to_re "tf8"))) (re.++ (re.union (re.++ (str.to_re "mac") (re.union (str.to_re "ce") (str.to_re "roman"))) (re.++ (str.to_re "cp") (re.union (re.++ (str.to_re "8") (re.union (re.++ (str.to_re "5") (re.union (str.to_re "0") (str.to_re "2"))) (str.to_re "66"))) (str.to_re "1256"))) (str.to_re "armscii8") (str.to_re "geostd8") (str.to_re "ascii") (str.to_re "keybcs2") (str.to_re "greek") (str.to_re "hebrew") (re.++ (str.to_re "koi8") (re.union (str.to_re "r") (str.to_re "u")))) (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "general_ci"))) (re.++ (re.union (str.to_re "dec8") (str.to_re "swe7")) (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "swedish_ci"))) (re.++ (re.union (str.to_re "hp8") (str.to_re "latin5")) (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "english_ci"))) (re.++ (re.union (str.to_re "big5") (re.++ (str.to_re "gb") (re.union (str.to_re "2312") (str.to_re "k")))) (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "chinese_ci"))) (re.++ (re.union (str.to_re "cp932") (str.to_re "eucjpms") (re.++ (re.union (str.to_re "s") (str.to_re "u")) (str.to_re "jis"))) (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "japanese_ci"))) (re.++ (str.to_re "euckr_") (re.union (str.to_re "bin") (str.to_re "korean_ci"))) (re.++ (str.to_re "tis620_") (re.union (str.to_re "bin") (str.to_re "thai_ci"))) (re.++ (str.to_re "latin1_") (re.union (str.to_re "bin") (re.++ (re.union (re.++ (re.union (str.to_re "dan") (str.to_re "span") (str.to_re "swed")) (str.to_re "ish")) (re.++ (str.to_re "german") (re.union (str.to_re "1") (str.to_re "2")))) (str.to_re "_ci")) (re.++ (str.to_re "general_c") (re.union (str.to_re "i") (str.to_re "s"))))) (re.++ (str.to_re "cp1250_") (re.union (str.to_re "bin") (str.to_re "czech_cs") (str.to_re "general_ci"))) (re.++ (str.to_re "latin2_") (re.union (str.to_re "bin") (str.to_re "czech_cs") (re.++ (re.union (str.to_re "general") (str.to_re "hungarian") (str.to_re "croatian")) (str.to_re "_ci")))) (re.++ (str.to_re "cp1257_") (re.union (str.to_re "bin") (re.++ (re.union (str.to_re "general") (str.to_re "lithuanian")) (str.to_re "_ci")))) (re.++ (str.to_re "latin7_") (re.union (str.to_re "bin") (re.++ (str.to_re "general_c") (re.union (str.to_re "i") (str.to_re "s"))) (str.to_re "estonian_cs"))) (re.++ (str.to_re "\u{a}cp1251_") (re.union (str.to_re "bin") (re.++ (re.union (str.to_re "general") (str.to_re "bulgarian") (str.to_re "ukrainian")) (str.to_re "_ci")) (str.to_re "general_cs")))))) -(check-sat) - -(exit) diff --git a/benchmarks/instance11705.smt2 b/benchmarks/instance11705.smt2 deleted file mode 100644 index 2c344ae0e..000000000 --- a/benchmarks/instance11705.smt2 +++ /dev/null @@ -1,23 +0,0 @@ -(set-info :smt-lib-version 2.6) -(set-logic QF_S) -(set-info :source | -Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu -Generated on: 2020-10-01 -Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark -Application: Evaluate solvers on real-world regex queries -Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau -Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. -|) -(set-info :license "https://creativecommons.org/licenses/by/4.0/") -(set-info :category "industrial") -(set-info :status unsat) - -(declare-const X String) -(assert (str.in_re X (re.++ (str.to_re "pjpoptwql/rlnj") (re.+ (re.range "0" "9")) (str.to_re "waiting") (re.+ (re.range "0" "9")) (str.to_re "ocllceclbhs/gth") (re.+ (re.union (re.range "0" "9") (re.range "A" "Z") (re.range "a" "z") (str.to_re "_"))) (str.to_re "gdvsotuqwsg/dxt.hdUser-Agent:\u{a}")))) -(assert (str.in_re X (re.++ (str.to_re "Host:") (re.range "0" "9") (str.to_re "Keylogger") (re.* re.allchar) (str.to_re "Onetrustyfiles.com\u{a}")))) -(assert (str.in_re X (re.++ ((_ re.loop 2 2) (re.range "0" "9")) (str.to_re "-") (re.union (str.to_re "Jan") (str.to_re "Feb") (str.to_re "Mar") (str.to_re "Apr") (str.to_re "May") (str.to_re "Jun") (str.to_re "Jul") (str.to_re "Aug") (str.to_re "Sep") (str.to_re "Oct") (str.to_re "Nov") (str.to_re "Dec") (str.to_re "jan") (str.to_re "feb") (str.to_re "mar") (str.to_re "apr") (str.to_re "may") (str.to_re "jun") (str.to_re "jul") (str.to_re "aug") (str.to_re "sep") (str.to_re "oct") (str.to_re "nov") (str.to_re "dec") (str.to_re "JAN") (str.to_re "FEB") (str.to_re "MAR") (str.to_re "APR") (str.to_re "MAY") (str.to_re "JUN") (str.to_re "JUL") (str.to_re "AUG") (str.to_re "SEP") (str.to_re "OCT") (str.to_re "NOV") (str.to_re "DEC")) (str.to_re "-") ((_ re.loop 4 4) (re.range "0" "9")) (str.to_re "\u{a}")))) -(assert (not (str.in_re X (re.++ (re.range "\u{80}" "\u{ff}") (str.to_re "\u{a}"))))) -(assert (str.in_re X (re.++ (str.to_re "/.xlw") (re.union (str.to_re "?") (str.to_re "\u{5c}") (str.to_re "/")) (str.to_re "/smiU\u{a}")))) -(check-sat) - -(exit) diff --git a/benchmarks/instance11745.smt2 b/benchmarks/instance11745.smt2 deleted file mode 100644 index 246a3f777..000000000 --- a/benchmarks/instance11745.smt2 +++ /dev/null @@ -1,21 +0,0 @@ -(set-info :smt-lib-version 2.6) -(set-logic QF_S) -(set-info :source | -Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu -Generated on: 2020-10-01 -Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark -Application: Evaluate solvers on real-world regex queries -Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau -Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. -|) -(set-info :license "https://creativecommons.org/licenses/by/4.0/") -(set-info :category "industrial") -(set-info :status unsat) - -(declare-const X String) -(assert (str.in_re X (re.union (str.to_re "EMA") (str.to_re "QCY") (str.to_re "SQZ") (str.to_re "ORM") (str.to_re "NQT") (str.to_re "WTN") (str.to_re "CBG") (str.to_re "QFO") (str.to_re "BEQ") (str.to_re "LKZ") (str.to_re "LTN") (str.to_re "KNF") (str.to_re "MHZ") (str.to_re "NWI") (str.to_re "CLF") (str.to_re "QUY") (str.to_re "SEN") (str.to_re "STN") (str.to_re "BEQ") (str.to_re "BQH") (str.to_re "LHR") (str.to_re "NHT") (str.to_re "LCY") (str.to_re "MME") (str.to_re "NCL") (str.to_re "BWF") (str.to_re "BLK") (str.to_re "CAX") (str.to_re "LPL") (str.to_re "MAN") (str.to_re "BBP") (str.to_re "BEX") (str.to_re "BZZ") (str.to_re "LGW") (str.to_re "SOU") (str.to_re "FAB") (str.to_re "OXF") (str.to_re "ESH") (str.to_re "QLA") (str.to_re "LYX") (str.to_re "KRH") (str.to_re "ODH") (str.to_re "RCS") (str.to_re "QUC") (str.to_re "BBS") (str.to_re "GLO") (str.to_re "EXT") (str.to_re "FFD") (str.to_re "BOH") (str.to_re "LYE") (str.to_re "NQY") (str.to_re "LEQ") (str.to_re "ISC") (str.to_re "UPV") (str.to_re "BRS") (str.to_re "YEO") (str.to_re "CVT") (str.to_re "BHX") (str.to_re "DSA") (str.to_re "HUY") (str.to_re "LBA") (str.to_re "HRT") (str.to_re "BFS") (str.to_re "BHD") (str.to_re "LDY") (str.to_re "ENK") (str.to_re "ABZ") (str.to_re "OBN") (str.to_re "BEB") (str.to_re "BRR") (str.to_re "CAL") (str.to_re "COL") (str.to_re "CSA") (str.to_re "NRL") (str.to_re "INV") (str.to_re "SCS") (str.to_re "DND") (str.to_re "LSI") (str.to_re "EOI") (str.to_re "EDI") (str.to_re "FIE") (str.to_re "FOA") (str.to_re "ILY") (str.to_re "FSS") (str.to_re "NDY") (str.to_re "ADX") (str.to_re "LMO") (str.to_re "OUK") (str.to_re "PSV") (str.to_re "PPW") (str.to_re "PIK") (str.to_re "GLA") (str.to_re "KOI") (str.to_re "PSL") (str.to_re "SYY") (str.to_re "SKL") (str.to_re "SOY") (str.to_re "LWK") (str.to_re "TRE") (str.to_re "WRY") (str.to_re "WHS") (str.to_re "WIC") (str.to_re "HAW") (str.to_re "CEG") (str.to_re "VLY") (str.to_re "SWS") (str.to_re "CWL") (str.to_re "DGX") (str.to_re "ACI") (str.to_re "GCI") (str.to_re "IOM") (str.to_re "JER\u{a}")))) -(assert (str.in_re X (re.++ (str.to_re "/User-Agent: ") ((_ re.loop 9 9) (re.range "A" "Z")) (str.to_re "\u{d}\u{a}/Hm\u{a}")))) -(assert (str.in_re X (re.++ (str.to_re "Admin") (re.+ (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "daosearch.comMyPostwww.raxsearch.comref=%user_id\u{a}")))) -(check-sat) - -(exit) diff --git a/benchmarks/instance11856.smt2 b/benchmarks/instance11856.smt2 deleted file mode 100644 index 0c9a4d020..000000000 --- a/benchmarks/instance11856.smt2 +++ /dev/null @@ -1,21 +0,0 @@ -(set-info :smt-lib-version 2.6) -(set-logic QF_S) -(set-info :source | -Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu -Generated on: 2020-10-01 -Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark -Application: Evaluate solvers on real-world regex queries -Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau -Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. -|) -(set-info :license "https://creativecommons.org/licenses/by/4.0/") -(set-info :category "industrial") -(set-info :status sat) - -(declare-const X String) -(assert (not (str.in_re X (re.++ (str.to_re "/filename=") (re.* (re.comp (str.to_re "\u{a}"))) (str.to_re ".addin/i\u{a}"))))) -(assert (not (str.in_re X (re.++ (str.to_re "//") ((_ re.loop 5 5) (re.range "0" "9")) (str.to_re ".jar/U\u{a}"))))) -(assert (str.in_re X (re.++ (re.union (str.to_re "big5") (re.++ (str.to_re "euc") (re.union (str.to_re "kr") (str.to_re "jpms"))) (str.to_re "binary") (str.to_re "greek") (str.to_re "tis620") (str.to_re "hebrew") (str.to_re "ascii") (str.to_re "swe7") (re.++ (str.to_re "koi8") (re.union (str.to_re "r") (str.to_re "u"))) (re.++ (re.union (str.to_re "u") (str.to_re "keyb")) (str.to_re "cs2")) (re.++ (re.union (str.to_re "dec") (str.to_re "hp") (str.to_re "utf") (str.to_re "geostd") (str.to_re "armscii")) (str.to_re "8")) (re.++ (str.to_re "gb") (re.union (str.to_re "k") (str.to_re "2312"))) (re.++ (str.to_re "cp") (re.union (re.++ (str.to_re "8") (re.union (re.++ (str.to_re "5") (re.union (str.to_re "0") (str.to_re "2"))) (str.to_re "66"))) (str.to_re "932") (re.++ (str.to_re "125") (re.union (str.to_re "0") (str.to_re "1") (str.to_re "6") (str.to_re "7"))))) (re.++ (str.to_re "latin") (re.union (str.to_re "1") (str.to_re "2") (str.to_re "5") (str.to_re "7"))) (re.++ (re.union (str.to_re "u") (str.to_re "s")) (str.to_re "jis")) (re.++ (str.to_re "mac") (re.union (str.to_re "ce") (str.to_re "roman")))) (str.to_re "\u{a}")))) -(check-sat) - -(exit) diff --git a/benchmarks/instance12204.smt2 b/benchmarks/instance12204.smt2 deleted file mode 100644 index 4a192538c..000000000 --- a/benchmarks/instance12204.smt2 +++ /dev/null @@ -1,22 +0,0 @@ -(set-info :smt-lib-version 2.6) -(set-logic QF_S) -(set-info :source | -Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu -Generated on: 2020-10-01 -Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark -Application: Evaluate solvers on real-world regex queries -Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau -Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. -|) -(set-info :license "https://creativecommons.org/licenses/by/4.0/") -(set-info :category "industrial") -(set-info :status unsat) - -(declare-const X String) -(assert (not (str.in_re X (re.++ (re.* (re.range "0" "9")) (re.+ (re.range "1" "9")) (re.* (re.range "0" "9")) (str.to_re "\u{a}"))))) -(assert (not (str.in_re X (re.++ (str.to_re "/.svg") (re.opt (str.to_re "z")) (re.union (str.to_re "?") (str.to_re "\u{5c}") (str.to_re "/")) (str.to_re "/smiU\u{a}"))))) -(assert (str.in_re X (re.++ (str.to_re "<") (re.opt (str.to_re "/")) (re.union (str.to_re "a") (str.to_re "abbr") (str.to_re "acronym") (str.to_re "address") (str.to_re "applet") (str.to_re "area") (str.to_re "b") (str.to_re "base") (str.to_re "basefont") (str.to_re "bdo") (str.to_re "big") (str.to_re "blockquote") (str.to_re "body") (str.to_re "br") (str.to_re "button") (str.to_re "caption") (str.to_re "center") (str.to_re "cite") (str.to_re "code") (str.to_re "col") (str.to_re "colgroup") (str.to_re "dd") (str.to_re "del") (str.to_re "dir") (str.to_re "div") (str.to_re "dfn") (str.to_re "dl") (str.to_re "dt") (str.to_re "em") (str.to_re "fieldset") (str.to_re "font") (str.to_re "form") (str.to_re "frame") (str.to_re "frameset") (re.++ (str.to_re "h") (re.range "1" "6")) (str.to_re "head") (str.to_re "hr") (str.to_re "html") (str.to_re "i") (str.to_re "iframe") (str.to_re "img") (str.to_re "input") (str.to_re "ins") (str.to_re "isindex") (str.to_re "kbd") (str.to_re "label") (str.to_re "legend") (str.to_re "li") (str.to_re "link") (str.to_re "map") (str.to_re "menu") (str.to_re "meta") (str.to_re "noframes") (str.to_re "noscript") (str.to_re "object") (str.to_re "ol") (str.to_re "optgroup") (str.to_re "option") (str.to_re "p") (str.to_re "param") (str.to_re "pre") (str.to_re "q") (str.to_re "s") (str.to_re "samp") (str.to_re "script") (str.to_re "select") (str.to_re "small") (str.to_re "span") (str.to_re "strike") (str.to_re "strong") (str.to_re "style") (str.to_re "sub") (str.to_re "sup") (str.to_re "table") (str.to_re "tbody") (str.to_re "td") (str.to_re "textarea") (str.to_re "tfoot") (str.to_re "th") (str.to_re "thead") (str.to_re "title") (str.to_re "tr") (str.to_re "tt") (str.to_re "u") (str.to_re "ul") (str.to_re "var") (str.to_re "xmp")) (re.* (re.union (re.* (re.union (re.++ (str.to_re "\u{22}") (re.* (re.comp (str.to_re "\u{22}"))) (str.to_re "\u{22}")) (re.++ (str.to_re "'") (re.* (re.comp (str.to_re "'"))) (str.to_re "'")))) (str.to_re "\u{22}") (str.to_re "'") (str.to_re ">"))) (str.to_re ">\u{a}")))) -(assert (str.in_re X (re.++ (str.to_re "/SOAPAction:") (re.* (re.union (str.to_re "\u{d}") (str.to_re "\u{a}"))) (str.to_re "Get") (re.union (str.to_re "ServerTime") (str.to_re "FileList") (str.to_re "File")) (str.to_re "\u{22}/i\u{a}")))) -(check-sat) - -(exit) diff --git a/benchmarks/instance12488.smt2 b/benchmarks/instance12488.smt2 deleted file mode 100644 index b62061cb5..000000000 --- a/benchmarks/instance12488.smt2 +++ /dev/null @@ -1,22 +0,0 @@ -(set-info :smt-lib-version 2.6) -(set-logic QF_S) -(set-info :source | -Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu -Generated on: 2020-10-01 -Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark -Application: Evaluate solvers on real-world regex queries -Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau -Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. -|) -(set-info :license "https://creativecommons.org/licenses/by/4.0/") -(set-info :category "industrial") -(set-info :status unsat) - -(declare-const X String) -(assert (not (str.in_re X (re.++ (re.range "1" "9") (re.range "0" "9") (re.range "0" "9") (re.range "0" "9") (re.range "0" "9") (re.range "0" "9") (str.to_re "\u{a}"))))) -(assert (str.in_re X (re.++ (str.to_re "/.s3m") (re.union (str.to_re "?") (str.to_re "\u{5c}") (str.to_re "/")) (str.to_re "/smiU\u{a}")))) -(assert (str.in_re X (re.++ ((_ re.loop 7 8) (re.range "0" "9")) (str.to_re "\u{a}0") (re.union (str.to_re "2") (str.to_re "|") (str.to_re "3") (str.to_re "4") (str.to_re "5") (str.to_re "6") (str.to_re "8") (str.to_re "9") (str.to_re "7"))))) -(assert (str.in_re X (re.++ (re.+ (re.union (str.to_re "_") (re.range "a" "z") (re.range "0" "9") (str.to_re "-"))) (re.* (re.++ (str.to_re ".") (re.+ (re.union (str.to_re "_") (re.range "a" "z") (re.range "0" "9") (str.to_re "-"))))) (str.to_re "@") (re.+ (re.union (re.range "a" "z") (re.range "0" "9"))) (re.opt (re.++ (re.opt (str.to_re "-")) (re.+ (re.union (re.range "a" "z") (re.range "0" "9"))))) (re.* (re.++ (str.to_re ".") (re.+ (re.union (re.range "a" "z") (re.range "0" "9"))) (re.opt (re.++ (re.opt (str.to_re "-")) (re.+ (re.union (re.range "a" "z") (re.range "0" "9"))))))) (str.to_re ".") (re.union ((_ re.loop 2 2) (re.range "a" "z")) (re.++ (str.to_re "xn") ((_ re.loop 2 2) (str.to_re "-")) ((_ re.loop 4 18) (re.union (re.range "a" "z") (re.range "0" "9")))) (str.to_re "arpa") (str.to_re "aero") (str.to_re "asia") (str.to_re "biz") (str.to_re "cat") (str.to_re "com") (str.to_re "coop") (str.to_re "edu") (str.to_re "gov") (str.to_re "info") (str.to_re "int") (str.to_re "jobs") (str.to_re "mil") (str.to_re "mobi") (str.to_re "museum") (str.to_re "name") (str.to_re "net") (str.to_re "org") (str.to_re "pro") (str.to_re "tel") (str.to_re "travel") (str.to_re "xxx")) (str.to_re "\u{a}")))) -(check-sat) - -(exit) diff --git a/benchmarks/instance12671.smt2 b/benchmarks/instance12671.smt2 deleted file mode 100644 index 164fbb7ed..000000000 --- a/benchmarks/instance12671.smt2 +++ /dev/null @@ -1,21 +0,0 @@ -(set-info :smt-lib-version 2.6) -(set-logic QF_S) -(set-info :source | -Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu -Generated on: 2020-10-01 -Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark -Application: Evaluate solvers on real-world regex queries -Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau -Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. -|) -(set-info :license "https://creativecommons.org/licenses/by/4.0/") -(set-info :category "industrial") -(set-info :status unsat) - -(declare-const X String) -(assert (str.in_re X (re.union (re.++ (re.union (re.++ (re.union (re.range "1" "9") (re.++ (str.to_re "0") (re.range "1" "9")) (re.++ (re.range "1" "2") (re.range "0" "9")) (str.to_re "30")) (str.to_re "-") (re.union (re.++ (re.union (str.to_re "A") (str.to_re ",") (str.to_re "a")) (re.union (str.to_re "P") (str.to_re ",") (str.to_re "p")) (re.union (str.to_re "R") (str.to_re ",") (str.to_re "r"))) (re.++ (re.union (str.to_re "J") (str.to_re ",") (str.to_re "j")) (re.union (str.to_re "U") (str.to_re ",") (str.to_re "u")) (re.union (str.to_re "N") (str.to_re ",") (str.to_re "n"))) (re.++ (re.union (str.to_re "S") (str.to_re ",") (str.to_re "s")) (re.union (str.to_re "E") (str.to_re ",") (str.to_re "e")) (re.union (str.to_re "P") (str.to_re ",") (str.to_re "p"))) (re.++ (re.union (str.to_re "N") (str.to_re ",") (str.to_re "n")) (re.union (str.to_re "O") (str.to_re ",") (str.to_re "o")) (re.union (str.to_re "V") (str.to_re ",") (str.to_re "v"))))) (re.++ (re.union (re.range "1" "9") (re.++ (str.to_re "0") (re.range "1" "9")) (re.++ (re.range "1" "2") (re.range "0" "9")) (re.++ (str.to_re "3") (re.range "0" "1"))) (str.to_re "-") (re.union (re.++ (re.union (str.to_re "J") (str.to_re ",") (str.to_re "j")) (re.union (str.to_re "A") (str.to_re ",") (str.to_re "a")) (re.union (str.to_re "N") (str.to_re ",") (str.to_re "n"))) (re.++ (re.union (str.to_re "M") (str.to_re ",") (str.to_re "m")) (re.union (str.to_re "A") (str.to_re ",") (str.to_re "a")) (re.union (str.to_re "R") (str.to_re ",") (str.to_re "r"))) (re.++ (re.union (str.to_re "M") (str.to_re ",") (str.to_re "m")) (re.union (str.to_re "A") (str.to_re ",") (str.to_re "a")) (re.union (str.to_re "Y") (str.to_re ",") (str.to_re "y"))) (re.++ (re.union (str.to_re "J") (str.to_re ",") (str.to_re "j")) (re.union (str.to_re "U") (str.to_re ",") (str.to_re "u")) (re.union (str.to_re "L") (str.to_re ",") (str.to_re "l"))) (re.++ (re.union (str.to_re "A") (str.to_re ",") (str.to_re "a")) (re.union (str.to_re "U") (str.to_re ",") (str.to_re "u")) (re.union (str.to_re "G") (str.to_re ",") (str.to_re "g"))) (re.++ (re.union (str.to_re "O") (str.to_re ",") (str.to_re "o")) (re.union (str.to_re "C") (str.to_re ",") (str.to_re "c")) (re.union (str.to_re "T") (str.to_re ",") (str.to_re "t"))) (re.++ (re.union (str.to_re "D") (str.to_re ",") (str.to_re "d")) (re.union (str.to_re "E") (str.to_re ",") (str.to_re "e")) (re.union (str.to_re "C") (str.to_re ",") (str.to_re "c")))))) (str.to_re "-") ((_ re.loop 4 4) (re.range "0" "9"))) (re.++ (re.union (re.range "1" "9") (re.++ (str.to_re "0") (re.range "1" "9")) (re.++ (str.to_re "1") (re.range "0" "9")) (re.++ (str.to_re "2") (re.range "0" "8"))) (str.to_re "--") ((_ re.loop 2 2) (re.range "0" "9")) (re.union (re.++ (re.union (str.to_re "0") (str.to_re "2") (str.to_re "4") (str.to_re "6") (str.to_re "8")) (re.union (str.to_re "1") (str.to_re "2") (str.to_re "3") (str.to_re "5") (str.to_re "6") (str.to_re "7") (str.to_re "9"))) (re.++ (re.union (str.to_re "1") (str.to_re "3") (str.to_re "5") (str.to_re "7") (str.to_re "9")) (re.union (str.to_re "0") (str.to_re "1") (str.to_re "3") (str.to_re "4") (str.to_re "5") (str.to_re "7") (str.to_re "8") (str.to_re "9")))) (re.union (str.to_re "F") (str.to_re ",") (str.to_re "f")) (re.union (str.to_re "E") (str.to_re ",") (str.to_re "e")) (re.union (str.to_re "B") (str.to_re ",") (str.to_re "b"))) (re.++ (str.to_re "\u{a}") (re.union (re.range "1" "9") (re.++ (str.to_re "0") (re.range "1" "9")) (re.++ (str.to_re "1") (re.range "0" "9")) (re.++ (str.to_re "2") (re.range "0" "9"))) (str.to_re "--") ((_ re.loop 2 2) (re.range "0" "9")) (re.union (re.++ (re.union (str.to_re "0") (str.to_re "2") (str.to_re "4") (str.to_re "6") (str.to_re "8")) (re.union (str.to_re "0") (str.to_re "4") (str.to_re "8"))) (re.++ (re.union (str.to_re "1") (str.to_re "3") (str.to_re "5") (str.to_re "7") (str.to_re "9")) (re.union (str.to_re "2") (str.to_re "6")))) (re.union (str.to_re "F") (str.to_re ",") (str.to_re "f")) (re.union (str.to_re "E") (str.to_re ",") (str.to_re "e")) (re.union (str.to_re "B") (str.to_re ",") (str.to_re "b")))))) -(assert (str.in_re X (re.union (re.++ (re.union (re.range "0" "9") (re.++ (re.range "0" "1") (re.range "0" "9")) (re.++ (str.to_re "2") (re.range "0" "3"))) (str.to_re ":") (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (re.union (str.to_re "AM") (str.to_re "PM") (str.to_re "am") (str.to_re "pm") (str.to_re "aM") (str.to_re "Am") (str.to_re "pM") (re.++ (str.to_re "P") ((_ re.loop 2 2) (str.to_re "m")))) (re.range "0" "5") (re.range "0" "9")) (re.++ (str.to_re "\u{a}") (re.union (re.range "0" "9") (re.++ (str.to_re "1") (re.range "0" "9")) (re.++ (str.to_re "2") (re.range "0" "3"))) (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (re.union (str.to_re "AM") (str.to_re "PM") (str.to_re "am") (str.to_re "pm") (str.to_re "aM") (str.to_re "Am") (str.to_re "pM") (re.++ (str.to_re "P") ((_ re.loop 2 2) (str.to_re "m")))))))) -(assert (str.in_re X (re.++ (str.to_re "Points") (re.+ (re.range "0" "9")) (str.to_re "Host:") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "toBasicwww.webcruiser.cc\u{a}")))) -(check-sat) - -(exit) diff --git a/benchmarks/instance12768.smt2 b/benchmarks/instance12768.smt2 deleted file mode 100644 index 361639b63..000000000 --- a/benchmarks/instance12768.smt2 +++ /dev/null @@ -1,22 +0,0 @@ -(set-info :smt-lib-version 2.6) -(set-logic QF_S) -(set-info :source | -Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu -Generated on: 2020-10-01 -Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark -Application: Evaluate solvers on real-world regex queries -Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau -Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. -|) -(set-info :license "https://creativecommons.org/licenses/by/4.0/") -(set-info :category "industrial") -(set-info :status unsat) - -(declare-const X String) -(assert (str.in_re X (re.++ (str.to_re "/User-Agent:") (re.+ (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "Ryeol") (re.+ (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "HTTP") (re.+ (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "Client") (re.+ (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "Class/smiH\u{a}")))) -(assert (str.in_re X (re.++ (str.to_re "Spyware") (re.+ (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "ToolBar") (re.+ (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "User-Agent:MM_RECO.EXEToClientonAlert\u{a}")))) -(assert (str.in_re X (re.++ (str.to_re "ver") (re.+ (re.range "0" "9")) (str.to_re "sports") (re.+ (re.union (re.range "0" "9") (re.range "A" "Z") (re.range "a" "z") (str.to_re "_"))) (str.to_re "whenu.com\u{13}wp-includes/feed.php?\u{a}")))) -(assert (str.in_re X (re.++ (str.to_re "qr/") (re.union (str.to_re "Alabama") (str.to_re "Alaska") (str.to_re "Arizona") (str.to_re "Arkansas") (str.to_re "California") (str.to_re "Colorado") (str.to_re "Connecticut") (str.to_re "Delaware") (str.to_re "Florida") (str.to_re "Georgia") (str.to_re "Hawaii") (str.to_re "Idaho") (str.to_re "Illinois") (str.to_re "Indiana") (str.to_re "Iowa") (str.to_re "Kansas") (str.to_re "Kentucky") (str.to_re "Louisiana") (str.to_re "Maine") (str.to_re "Maryland") (str.to_re "Massachusetts") (str.to_re "Michigan") (str.to_re "Minnesota") (str.to_re "Mississippi") (str.to_re "Missouri") (str.to_re "Montana") (str.to_re "Nebraska") (str.to_re "Nevada") (re.++ (str.to_re "New") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Hampshire")) (re.++ (str.to_re "New") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Jersey")) (re.++ (str.to_re "New") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Mexico")) (re.++ (str.to_re "New") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "York")) (re.++ (str.to_re "North") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Carolina")) (re.++ (str.to_re "North") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Dakota")) (str.to_re "Ohio") (str.to_re "Oklahoma") (str.to_re "Oregon") (str.to_re "Pennsylvania") (re.++ (str.to_re "Rhode") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Island")) (re.++ (str.to_re "South") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Carolina")) (re.++ (str.to_re "South") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Dakota")) (str.to_re "Tennessee") (str.to_re "Texas") (str.to_re "Utah") (str.to_re "Vermont") (str.to_re "Virginia") (str.to_re "Washington") (re.++ (str.to_re "West") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Virginia")) (str.to_re "Wisconsin") (str.to_re "Wyoming")) (str.to_re "/\u{a}")))) -(check-sat) - -(exit) diff --git a/benchmarks/instance12833.smt2 b/benchmarks/instance12833.smt2 deleted file mode 100644 index 1cbbd4099..000000000 --- a/benchmarks/instance12833.smt2 +++ /dev/null @@ -1,22 +0,0 @@ -(set-info :smt-lib-version 2.6) -(set-logic QF_S) -(set-info :source | -Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu -Generated on: 2020-10-01 -Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark -Application: Evaluate solvers on real-world regex queries -Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau -Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. -|) -(set-info :license "https://creativecommons.org/licenses/by/4.0/") -(set-info :category "industrial") -(set-info :status unsat) - -(declare-const X String) -(assert (str.in_re X (re.++ (str.to_re "|Connected") (re.+ (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "adblock.linkz.com\u{a}")))) -(assert (str.in_re X (re.++ (str.to_re "//u\u{a}") (re.range "\u{0}" "\u{ff}") (re.* (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")))))) -(assert (str.in_re X (re.++ (re.* (re.++ (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.* (re.union (re.++ (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.* (re.++ (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8")))) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.* (re.++ (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7")))) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.* (re.++ (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7")))) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7"))) (re.++ (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.* (re.++ (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7")))) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.* (re.++ (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8")))) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.* (re.++ (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8")))) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8"))) (re.++ (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.* (re.++ (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8")))) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8"))) (re.++ (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.* (re.++ (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7")))) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7"))))) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))))) (str.to_re "\u{a}")))) -(assert (str.in_re X (re.++ (str.to_re "/.pui") (re.union (str.to_re "?") (str.to_re "\u{5c}") (str.to_re "/")) (str.to_re "/smiU\u{a}")))) -(check-sat) - -(exit) diff --git a/benchmarks/instance13062.smt2 b/benchmarks/instance13062.smt2 deleted file mode 100644 index 06bb16d4e..000000000 --- a/benchmarks/instance13062.smt2 +++ /dev/null @@ -1,23 +0,0 @@ -(set-info :smt-lib-version 2.6) -(set-logic QF_S) -(set-info :source | -Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu -Generated on: 2020-10-01 -Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark -Application: Evaluate solvers on real-world regex queries -Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau -Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. -|) -(set-info :license "https://creativecommons.org/licenses/by/4.0/") -(set-info :category "industrial") -(set-info :status unsat) - -(declare-const X String) -(assert (not (str.in_re X (re.++ (str.to_re "/filename") (re.* (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "=") (re.* (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (re.* (re.union (str.to_re "\u{d}") (str.to_re "\u{a}"))) (str.to_re ".swf") (re.union (str.to_re "\u{22}") (str.to_re "'") (str.to_re ";") (str.to_re "\u{d}") (str.to_re "\u{a}") (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "/i\u{a}"))))) -(assert (not (str.in_re X (re.++ (re.union (re.++ (str.to_re "A") (re.union (str.to_re "L") (str.to_re "K") (str.to_re "S") (str.to_re "Z") (str.to_re "R") (str.to_re "A") (str.to_re "E") (str.to_re "P"))) (re.++ (str.to_re "C") (re.union (str.to_re "A") (str.to_re "O") (str.to_re "T"))) (re.++ (str.to_re "D") (re.union (str.to_re "E") (str.to_re "C"))) (re.++ (str.to_re "F") (re.union (str.to_re "L") (str.to_re "M"))) (re.++ (str.to_re "G") (re.union (str.to_re "A") (str.to_re "U"))) (str.to_re "HI") (re.++ (str.to_re "I") (re.union (str.to_re "A") (str.to_re "D") (str.to_re "L") (str.to_re "N"))) (re.++ (str.to_re "K") (re.union (str.to_re "S") (str.to_re "Y"))) (str.to_re "LA") (re.++ (str.to_re "M") (re.union (str.to_re "A") (str.to_re "D") (str.to_re "E") (str.to_re "H") (str.to_re "I") (str.to_re "N") (str.to_re "O") (str.to_re "P") (str.to_re "S") (str.to_re "T"))) (re.++ (str.to_re "N") (re.union (str.to_re "C") (str.to_re "D") (str.to_re "E") (str.to_re "H") (str.to_re "J") (str.to_re "M") (str.to_re "V") (str.to_re "Y"))) (re.++ (str.to_re "O") (re.union (str.to_re "H") (str.to_re "K") (str.to_re "R"))) (re.++ (str.to_re "P") (re.union (str.to_re "A") (str.to_re "R") (str.to_re "W"))) (str.to_re "RI") (re.++ (str.to_re "S") (re.union (str.to_re "C") (str.to_re "D"))) (re.++ (str.to_re "T") (re.union (str.to_re "N") (str.to_re "X"))) (str.to_re "UT") (re.++ (str.to_re "V") (re.union (str.to_re "A") (str.to_re "I") (str.to_re "T"))) (re.++ (str.to_re "W") (re.union (str.to_re "A") (str.to_re "I") (str.to_re "V") (str.to_re "Y")))) (str.to_re "\u{a}"))))) -(assert (str.in_re X (re.++ (str.to_re "/.wmv") (re.union (str.to_re "?") (str.to_re "\u{5c}") (str.to_re "/")) (str.to_re "/smiU\u{a}")))) -(assert (not (str.in_re X (re.++ (str.to_re "User-Agent:") (re.* re.allchar) (str.to_re "Host:") (re.* re.allchar) (str.to_re "w3whowww.sogou.com\u{a}"))))) -(assert (str.in_re X (re.++ (str.to_re "Guarded") (re.+ (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "ready") (re.+ (re.union (re.range "0" "9") (re.range "A" "Z") (re.range "a" "z") (str.to_re "_"))) (str.to_re "PARSERHost:A-311ServerUser-Agent:scn.mystoretoolbar.com\u{13}\u{a}")))) -(check-sat) - -(exit) diff --git a/benchmarks/instance13106.smt2 b/benchmarks/instance13106.smt2 deleted file mode 100644 index f0a3462e3..000000000 --- a/benchmarks/instance13106.smt2 +++ /dev/null @@ -1,23 +0,0 @@ -(set-info :smt-lib-version 2.6) -(set-logic QF_S) -(set-info :source | -Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu -Generated on: 2020-10-01 -Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark -Application: Evaluate solvers on real-world regex queries -Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau -Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. -|) -(set-info :license "https://creativecommons.org/licenses/by/4.0/") -(set-info :category "industrial") -(set-info :status unsat) - -(declare-const X String) -(assert (str.in_re X (re.++ (str.to_re "security") (re.+ (re.range "0" "9")) (str.to_re "Redirector\u{22}ServerHost:X-Mailer:\u{13}\u{a}")))) -(assert (str.in_re X (re.++ (re.opt (re.++ (str.to_re "1") (re.union (re.++ (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "-") (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")))) (re.++ (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re ".") (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")))) (re.++ (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "/") (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")))) (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")))) (re.opt (re.++ (re.opt (str.to_re "(")) ((_ re.loop 1 1) (re.range "2" "9")) ((_ re.loop 2 2) (re.range "0" "9")) (re.opt (str.to_re ")")) (re.opt (re.union (re.++ (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "-") (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")))) (re.++ (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re ".") (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")))) (re.++ (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "/") (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")))) (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))))) ((_ re.loop 3 3) (re.range "0" "9")) (re.opt (re.union (re.++ (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "-") (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")))) (re.++ (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re ".") (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")))) (re.++ (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "/") (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")))) (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) ((_ re.loop 4 4) (re.range "0" "9")) (str.to_re "\u{a}")))) -(assert (str.in_re X (re.++ (str.to_re "/filename=") (re.* (re.comp (str.to_re "\u{a}"))) (str.to_re ".svg/i\u{a}")))) -(assert (not (str.in_re X (str.to_re "MyHost:toHost:WinSessionwww.urlblaze.netResultHost:\u{a}")))) -(assert (not (str.in_re X (re.++ (str.to_re "/filename=") (re.opt (re.union (str.to_re "\u{22}") (str.to_re "'"))) (re.* (re.comp (str.to_re "\u{a}"))) (str.to_re ".pif") (re.union (str.to_re "\u{22}") (str.to_re "'") (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "/si\u{a}"))))) -(check-sat) - -(exit) diff --git a/benchmarks/instance13975.smt2 b/benchmarks/instance13975.smt2 deleted file mode 100644 index af0baede7..000000000 --- a/benchmarks/instance13975.smt2 +++ /dev/null @@ -1,22 +0,0 @@ -(set-info :smt-lib-version 2.6) -(set-logic QF_S) -(set-info :source | -Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu -Generated on: 2020-10-01 -Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark -Application: Evaluate solvers on real-world regex queries -Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau -Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. -|) -(set-info :license "https://creativecommons.org/licenses/by/4.0/") -(set-info :category "industrial") -(set-info :status unsat) - -(declare-const X String) -(assert (str.in_re X (re.++ (re.opt (str.to_re "D")) (re.opt (re.union (str.to_re "-") (str.to_re "D"))) ((_ re.loop 5 5) (re.range "0" "9")) (str.to_re "\u{a}")))) -(assert (str.in_re X (re.union (re.++ (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "general") (str.to_re "unicode") (str.to_re "roman") (str.to_re "slovak") (str.to_re "czech") (str.to_re "icelandic") (re.++ (re.union (str.to_re "latv") (str.to_re "pers")) (str.to_re "ian")) (re.++ (re.union (str.to_re "dan") (str.to_re "pol") (str.to_re "span") (str.to_re "swed") (str.to_re "turk")) (str.to_re "ish")) (str.to_re "spanish2") (re.++ (re.union (str.to_re "esto") (str.to_re "lithua") (str.to_re "roma") (str.to_re "slove")) (str.to_re "nian_ci"))) (str.to_re "u") (re.union (str.to_re "cs2") (str.to_re "tf8"))) (re.++ (re.union (re.++ (str.to_re "mac") (re.union (str.to_re "ce") (str.to_re "roman"))) (re.++ (str.to_re "cp") (re.union (re.++ (str.to_re "8") (re.union (re.++ (str.to_re "5") (re.union (str.to_re "0") (str.to_re "2"))) (str.to_re "66"))) (str.to_re "1256"))) (str.to_re "armscii8") (str.to_re "geostd8") (str.to_re "ascii") (str.to_re "keybcs2") (str.to_re "greek") (str.to_re "hebrew") (re.++ (str.to_re "koi8") (re.union (str.to_re "r") (str.to_re "u")))) (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "general_ci"))) (re.++ (re.union (str.to_re "dec8") (str.to_re "swe7")) (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "swedish_ci"))) (re.++ (re.union (str.to_re "hp8") (str.to_re "latin5")) (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "english_ci"))) (re.++ (re.union (str.to_re "big5") (re.++ (str.to_re "gb") (re.union (str.to_re "2312") (str.to_re "k")))) (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "chinese_ci"))) (re.++ (re.union (str.to_re "cp932") (str.to_re "eucjpms") (re.++ (re.union (str.to_re "s") (str.to_re "u")) (str.to_re "jis"))) (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "japanese_ci"))) (re.++ (str.to_re "euckr_") (re.union (str.to_re "bin") (str.to_re "korean_ci"))) (re.++ (str.to_re "tis620_") (re.union (str.to_re "bin") (str.to_re "thai_ci"))) (re.++ (str.to_re "latin1_") (re.union (str.to_re "bin") (re.++ (re.union (re.++ (re.union (str.to_re "dan") (str.to_re "span") (str.to_re "swed")) (str.to_re "ish")) (re.++ (str.to_re "german") (re.union (str.to_re "1") (str.to_re "2")))) (str.to_re "_ci")) (re.++ (str.to_re "general_c") (re.union (str.to_re "i") (str.to_re "s"))))) (re.++ (str.to_re "cp1250_") (re.union (str.to_re "bin") (str.to_re "czech_cs") (str.to_re "general_ci"))) (re.++ (str.to_re "latin2_") (re.union (str.to_re "bin") (str.to_re "czech_cs") (re.++ (re.union (str.to_re "general") (str.to_re "hungarian") (str.to_re "croatian")) (str.to_re "_ci")))) (re.++ (str.to_re "cp1257_") (re.union (str.to_re "bin") (re.++ (re.union (str.to_re "general") (str.to_re "lithuanian")) (str.to_re "_ci")))) (re.++ (str.to_re "latin7_") (re.union (str.to_re "bin") (re.++ (str.to_re "general_c") (re.union (str.to_re "i") (str.to_re "s"))) (str.to_re "estonian_cs"))) (re.++ (str.to_re "\u{a}cp1251_") (re.union (str.to_re "bin") (re.++ (re.union (str.to_re "general") (str.to_re "bulgarian") (str.to_re "ukrainian")) (str.to_re "_ci")) (str.to_re "general_cs")))))) -(assert (not (str.in_re X (re.++ (str.to_re "/.cgm") (re.union (str.to_re "?") (str.to_re "\u{5c}") (str.to_re "/")) (str.to_re "/smiU\u{a}"))))) -(assert (str.in_re X (re.++ (re.union (str.to_re "\u{5c}") (str.to_re "s") (str.to_re "+") (str.to_re ",")) (str.to_re "\u{a}")))) -(check-sat) - -(exit) diff --git a/benchmarks/instance14260.smt2 b/benchmarks/instance14260.smt2 deleted file mode 100644 index bf36054fc..000000000 --- a/benchmarks/instance14260.smt2 +++ /dev/null @@ -1,23 +0,0 @@ -(set-info :smt-lib-version 2.6) -(set-logic QF_S) -(set-info :source | -Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu -Generated on: 2020-10-01 -Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark -Application: Evaluate solvers on real-world regex queries -Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau -Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. -|) -(set-info :license "https://creativecommons.org/licenses/by/4.0/") -(set-info :category "industrial") -(set-info :status unsat) - -(declare-const X String) -(assert (not (str.in_re X (re.++ (str.to_re "")) (re.* re.allchar) (str.to_re "\u{a}"))))) -(assert (str.in_re X (re.++ (re.union (re.++ (re.range "0" "1") (re.range "0" "9")) (re.++ (str.to_re "2") (re.range "0" "3"))) (str.to_re ":\u{a}") (re.range "0" "5") (re.range "0" "9")))) -(assert (str.in_re X (re.++ (str.to_re "Password=\u{22}") (re.union (re.++ (str.to_re "{") (re.+ re.allchar) (str.to_re "}") (re.+ (re.union (re.range "0" "9") (re.range "a" "z") (re.range "A" "Z"))) (re.* (str.to_re "="))) (re.+ (re.union (re.range "0" "9") (re.range "a" "z") (re.range "A" "Z")))) (str.to_re "\u{22}\u{a}")))) -(assert (str.in_re X (re.++ (re.union (re.++ (re.union (re.++ (re.union (re.++ (re.opt (str.to_re "0")) (re.range "1" "9")) (re.++ (re.range "1" "2") (re.range "0" "9")) (re.++ (str.to_re "3") (re.range "0" "1"))) (str.to_re "-") (re.union (re.++ (re.union (str.to_re "j") (str.to_re "J")) (re.union (str.to_re "a") (str.to_re "A")) (re.union (str.to_re "n") (str.to_re "N"))) (re.++ (re.union (str.to_re "m") (str.to_re "M")) (re.union (str.to_re "a") (str.to_re "A")) (re.union (str.to_re "r") (str.to_re "R"))) (re.++ (re.union (str.to_re "m") (str.to_re "M")) (re.union (str.to_re "a") (str.to_re "A")) (re.union (str.to_re "y") (str.to_re "Y"))) (re.++ (re.union (str.to_re "j") (str.to_re "J")) (re.union (str.to_re "u") (str.to_re "U")) (re.union (str.to_re "l") (str.to_re "L"))) (re.++ (re.union (str.to_re "a") (str.to_re "A")) (re.union (str.to_re "u") (str.to_re "U")) (re.union (str.to_re "g") (str.to_re "G"))) (re.++ (re.union (str.to_re "o") (str.to_re "O")) (re.union (str.to_re "c") (str.to_re "C")) (re.union (str.to_re "t") (str.to_re "T"))) (re.++ (re.union (str.to_re "d") (str.to_re "D")) (re.union (str.to_re "e") (str.to_re "E")) (re.union (str.to_re "c") (str.to_re "C"))))) (re.++ (re.union (re.++ (re.opt (str.to_re "0")) (re.range "1" "9")) (re.++ (re.range "1" "2") (re.range "0" "9")) (str.to_re "30")) (str.to_re "-") (re.union (re.++ (re.union (str.to_re "a") (str.to_re "A")) (re.union (str.to_re "p") (str.to_re "P")) (re.union (str.to_re "r") (str.to_re "R"))) (re.++ (re.union (str.to_re "j") (str.to_re "J")) (re.union (str.to_re "u") (str.to_re "U")) (re.union (str.to_re "n") (str.to_re "N"))) (re.++ (re.union (str.to_re "s") (str.to_re "S")) (re.union (str.to_re "e") (str.to_re "E")) (re.union (str.to_re "p") (str.to_re "P"))) (re.++ (re.union (str.to_re "n") (str.to_re "N")) (re.union (str.to_re "o") (str.to_re "O")) (re.union (str.to_re "v") (str.to_re "V"))))) (re.++ (re.union (re.++ (re.opt (str.to_re "0")) (re.range "1" "9")) (re.++ (str.to_re "1") (re.range "0" "9")) (re.++ (str.to_re "2") (re.range "0" "8"))) (str.to_re "-") (re.union (str.to_re "f") (str.to_re "F")) (re.union (str.to_re "e") (str.to_re "E")) (re.union (str.to_re "b") (str.to_re "B")))) (str.to_re "-20") (re.union (re.++ (re.union (str.to_re "1") (str.to_re "3") (str.to_re "5") (str.to_re "7") (str.to_re "9")) (re.union (str.to_re "0") (str.to_re "1") (str.to_re "3") (str.to_re "4") (str.to_re "5") (str.to_re "7") (str.to_re "8") (str.to_re "9"))) (re.++ (re.union (str.to_re "2") (str.to_re "4") (str.to_re "6") (str.to_re "8")) (re.union (str.to_re "1") (str.to_re "2") (str.to_re "3") (str.to_re "5") (str.to_re "6") (str.to_re "7") (str.to_re "9"))))) (re.++ (re.union (re.++ (re.union (re.++ (re.opt (str.to_re "0")) (re.range "1" "9")) (re.++ (re.range "1" "2") (re.range "0" "9")) (re.++ (str.to_re "3") (re.range "0" "1"))) (str.to_re "-") (re.union (re.++ (re.union (str.to_re "j") (str.to_re "J")) (re.union (str.to_re "a") (str.to_re "A")) (re.union (str.to_re "n") (str.to_re "N"))) (re.++ (re.union (str.to_re "m") (str.to_re "M")) (re.union (str.to_re "a") (str.to_re "A")) (re.union (str.to_re "r") (str.to_re "R"))) (re.++ (re.union (str.to_re "m") (str.to_re "M")) (re.union (str.to_re "a") (str.to_re "A")) (re.union (str.to_re "y") (str.to_re "Y"))) (re.++ (re.union (str.to_re "j") (str.to_re "J")) (re.union (str.to_re "u") (str.to_re "U")) (re.union (str.to_re "l") (str.to_re "L"))) (re.++ (re.union (str.to_re "a") (str.to_re "A")) (re.union (str.to_re "u") (str.to_re "U")) (re.union (str.to_re "g") (str.to_re "G"))) (re.++ (re.union (str.to_re "o") (str.to_re "O")) (re.union (str.to_re "c") (str.to_re "C")) (re.union (str.to_re "t") (str.to_re "T"))) (re.++ (re.union (str.to_re "d") (str.to_re "D")) (re.union (str.to_re "e") (str.to_re "E")) (re.union (str.to_re "c") (str.to_re "C"))))) (re.++ (re.union (re.++ (re.opt (str.to_re "0")) (re.range "1" "9")) (re.++ (re.range "1" "2") (re.range "0" "9")) (str.to_re "30")) (str.to_re "-") (re.union (re.++ (re.union (str.to_re "a") (str.to_re "A")) (re.union (str.to_re "p") (str.to_re "P")) (re.union (str.to_re "r") (str.to_re "R"))) (re.++ (re.union (str.to_re "j") (str.to_re "J")) (re.union (str.to_re "u") (str.to_re "U")) (re.union (str.to_re "n") (str.to_re "N"))) (re.++ (re.union (str.to_re "s") (str.to_re "S")) (re.union (str.to_re "e") (str.to_re "E")) (re.union (str.to_re "p") (str.to_re "P"))) (re.++ (re.union (str.to_re "n") (str.to_re "N")) (re.union (str.to_re "o") (str.to_re "O")) (re.union (str.to_re "v") (str.to_re "V"))))) (re.++ (re.union (re.++ (re.opt (str.to_re "0")) (re.range "1" "9")) (re.++ (str.to_re "1") (re.range "0" "9")) (re.++ (str.to_re "2") (re.range "0" "9"))) (str.to_re "-") (re.union (str.to_re "f") (str.to_re "F")) (re.union (str.to_re "e") (str.to_re "E")) (re.union (str.to_re "b") (str.to_re "B")))) (str.to_re "-20") (re.union (re.++ (re.union (str.to_re "1") (str.to_re "3") (str.to_re "5") (str.to_re "7") (str.to_re "9")) (re.union (str.to_re "2") (str.to_re "6"))) (re.++ (re.union (str.to_re "2") (str.to_re "4") (str.to_re "6") (str.to_re "8")) (re.union (str.to_re "0") (str.to_re "4") (str.to_re "8")))))) (str.to_re "\u{a}")))) -(assert (not (str.in_re X (re.union (str.to_re "100") ((_ re.loop 1 2) (re.range "0" "9")) (re.++ ((_ re.loop 1 2) (re.range "0" "9")) (str.to_re ",") ((_ re.loop 1 3) (re.range "0" "9")) (str.to_re "\u{a}")))))) -(check-sat) - -(exit) diff --git a/benchmarks/instance14326.smt2 b/benchmarks/instance14326.smt2 deleted file mode 100644 index 35b8ab5c2..000000000 --- a/benchmarks/instance14326.smt2 +++ /dev/null @@ -1,21 +0,0 @@ -(set-info :smt-lib-version 2.6) -(set-logic QF_S) -(set-info :source | -Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu -Generated on: 2020-10-01 -Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark -Application: Evaluate solvers on real-world regex queries -Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau -Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. -|) -(set-info :license "https://creativecommons.org/licenses/by/4.0/") -(set-info :category "industrial") -(set-info :status sat) - -(declare-const X String) -(assert (not (str.in_re X (re.union (re.++ (re.union (str.to_re "Jan") (str.to_re "Feb") (str.to_re "Mar") (str.to_re "Apr") (str.to_re "May") (str.to_re "Jun") (str.to_re "Jul") (str.to_re "Aug") (str.to_re "Sep") (str.to_re "Oct") (str.to_re "Nov") (str.to_re "Dec")) (re.* (str.to_re ",")) (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (re.* (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) ((_ re.loop 4 4) (re.range "0" "9"))) (re.++ (re.union (str.to_re "jan") (str.to_re "feb") (str.to_re "mar") (str.to_re "apr") (str.to_re "may") (str.to_re "jun") (str.to_re "jul") (str.to_re "aug") (str.to_re "sep") (str.to_re "oct") (str.to_re "nov") (str.to_re "dec")) (re.* (str.to_re ",")) (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) ((_ re.loop 4 4) (re.range "0" "9"))) (re.++ (re.union (str.to_re "January") (str.to_re "February") (str.to_re "March") (str.to_re "April") (str.to_re "May") (str.to_re "June") (str.to_re "July") (str.to_re "August") (str.to_re "September") (str.to_re "October") (str.to_re "November") (str.to_re "December")) (re.* (str.to_re ",")) (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) ((_ re.loop 4 4) (re.range "0" "9"))) (re.++ (re.union (str.to_re "january") (str.to_re "february") (str.to_re "march") (str.to_re "april") (str.to_re "may") (str.to_re "june") (str.to_re "july") (str.to_re "august") (str.to_re "september") (str.to_re "october") (str.to_re "november") (str.to_re "december")) (re.* (str.to_re ",")) (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) ((_ re.loop 4 4) (re.range "0" "9")) (str.to_re "\u{a}")))))) -(assert (not (str.in_re X (re.++ (str.to_re "//jdb/inf.php?id=") ((_ re.loop 32 32) (re.union (re.range "a" "f") (re.range "0" "9"))) (str.to_re "/Ui\u{a}"))))) -(assert (not (str.in_re X (re.++ (re.* (re.opt (re.range "0" "9"))) (re.opt (re.++ (str.to_re ".") (re.union ((_ re.loop 1 1) (re.range "0" "9")) ((_ re.loop 2 2) (re.range "0" "9"))))) (str.to_re "\u{a}"))))) -(check-sat) - -(exit) diff --git a/benchmarks/instance14382.smt2 b/benchmarks/instance14382.smt2 deleted file mode 100644 index 72c67b77c..000000000 --- a/benchmarks/instance14382.smt2 +++ /dev/null @@ -1,21 +0,0 @@ -(set-info :smt-lib-version 2.6) -(set-logic QF_S) -(set-info :source | -Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu -Generated on: 2020-10-01 -Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark -Application: Evaluate solvers on real-world regex queries -Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau -Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. -|) -(set-info :license "https://creativecommons.org/licenses/by/4.0/") -(set-info :category "industrial") -(set-info :status unsat) - -(declare-const X String) -(assert (str.in_re X (re.++ (str.to_re "~/") (re.union (re.range "0" "9") (re.range "a" "z") (re.range "A" "Z") (str.to_re "_")) (re.* (re.union (re.range "0" "9") (re.range "a" "z") (re.range "A" "Z") (str.to_re "/") (str.to_re "_") (str.to_re "-"))) (str.to_re ".") (re.+ (re.union (re.range "0" "9") (re.range "a" "z") (re.range "A" "Z") (str.to_re "_") (str.to_re "-"))) (str.to_re "\u{a}")))) -(assert (str.in_re X (re.++ (re.opt (str.to_re "-")) (re.opt (str.to_re ",")) (re.union (re.++ ((_ re.loop 1 3) (re.range "0" "9")) (re.* (re.++ (str.to_re ".") ((_ re.loop 3 3) (re.range "0" "9"))))) (re.+ (re.range "0" "9"))) (re.opt (re.++ (str.to_re ",") ((_ re.loop 2 2) (re.range "0" "9")))) (str.to_re "\u{a}")))) -(assert (not (str.in_re X (re.++ (re.union (str.to_re "big5") (re.++ (str.to_re "euc") (re.union (str.to_re "kr") (str.to_re "jpms"))) (str.to_re "binary") (str.to_re "greek") (str.to_re "tis620") (str.to_re "hebrew") (str.to_re "ascii") (str.to_re "swe7") (re.++ (str.to_re "koi8") (re.union (str.to_re "r") (str.to_re "u"))) (re.++ (re.union (str.to_re "u") (str.to_re "keyb")) (str.to_re "cs2")) (re.++ (re.union (str.to_re "dec") (str.to_re "hp") (str.to_re "utf") (str.to_re "geostd") (str.to_re "armscii")) (str.to_re "8")) (re.++ (str.to_re "gb") (re.union (str.to_re "k") (str.to_re "2312"))) (re.++ (str.to_re "cp") (re.union (re.++ (str.to_re "8") (re.union (re.++ (str.to_re "5") (re.union (str.to_re "0") (str.to_re "2"))) (str.to_re "66"))) (str.to_re "932") (re.++ (str.to_re "125") (re.union (str.to_re "0") (str.to_re "1") (str.to_re "6") (str.to_re "7"))))) (re.++ (str.to_re "latin") (re.union (str.to_re "1") (str.to_re "2") (str.to_re "5") (str.to_re "7"))) (re.++ (re.union (str.to_re "u") (str.to_re "s")) (str.to_re "jis")) (re.++ (str.to_re "mac") (re.union (str.to_re "ce") (str.to_re "roman")))) (str.to_re "\u{a}"))))) -(check-sat) - -(exit)