From 6d4d1cb7974483f1762f349c049d522df7b11e10 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hans-J=C3=B6rg=20Schurr?= Date: Wed, 3 May 2023 11:39:47 -0500 Subject: [PATCH] test --- .../20230503-test/regex-049-fuzz-fuzz.smt2 | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 non-incremental/QF_UF/20230503-test/regex-049-fuzz-fuzz.smt2 diff --git a/non-incremental/QF_UF/20230503-test/regex-049-fuzz-fuzz.smt2 b/non-incremental/QF_UF/20230503-test/regex-049-fuzz-fuzz.smt2 new file mode 100644 index 0000000000..ded83c015b --- /dev/null +++ b/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)