test

non-incremental/QF_UF/20230503-test/regex-049-fuzz-fuzz.smt2

@@ -0,0 +1,23 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_UF)
+(set-info :source |
+Generated by: Dmitry Blotsky1, Federico Mora, Murphy Berzish, Yunhui Zheng, Ifaz Kabir, Vijay Ganesh, Zhengyang Lu
+Generated on: 2018-01-24
+Generator: StringFuzz
+Application: Evaluate string solvers
+Target solver: Z3str3, CVC4, Z3str2, Norn
+Publications: Blotsky, D., Mora, F., Berzish, M., Zheng, Y., Kabir, I., & Ganesh, V. (2018). Stringfuzz: A fuzzer for string solvers. In CAV 2018.
+Description: transformed by StringFuzz, a modular string and regex fuzzer, from an industrial benchmark
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "random")
+(set-info :status unknown)
+
+(declare-const key String)
+(declare-const val String)
+(assert (str.in_re key (re.+ (re.range "0" "2"))))
+(assert (<= 9 (str.len key)))
+(assert (>= 5 (str.to.int key)))
+(check-sat)
+
+(exit)