diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-18 11:35:24 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-18 11:35:24 -0500 |
commit | d091aa8d85e6336b469c312b9cc4c4e426a82094 (patch) | |
tree | 174c3fbcac3b81b27d1efb49b411490a3142d4ea /test | |
parent | 15128d91b6bdbff4141417855743f910950f9cc8 (diff) | |
parent | e040d5e9e9d8c01138b4b961a1118b7342735d87 (diff) |
Merge branch 'master' into fixNightlyCompfixNightlyComp
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress0/strings/issue5090.smt2 | 32 |
2 files changed, 33 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index c6f3b85f5..5f9465562 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -988,6 +988,7 @@ set(regress_0_tests regress0/strings/issue4674-recomp-nf.smt2 regress0/strings/issue4820.smt2 regress0/strings/issue4915.smt2 + regress0/strings/issue5090.smt2 regress0/strings/itos-entail.smt2 regress0/strings/large-model.smt2 regress0/strings/leadingzero001.smt2 diff --git a/test/regress/regress0/strings/issue5090.smt2 b/test/regress/regress0/strings/issue5090.smt2 new file mode 100644 index 000000000..44a57d4d2 --- /dev/null +++ b/test/regress/regress0/strings/issue5090.smt2 @@ -0,0 +1,32 @@ +; COMMAND-LINE: --strings-exp --incremental +(set-logic QF_S) +(declare-const Str0 String) +(declare-const Str1 String) +(declare-const Str2 String) +(declare-const Str3 String) +(declare-const Str4 String) +(declare-const Str5 String) +(declare-const Str6 String) +(declare-const Str7 String) +(declare-const Str8 String) +(declare-const Str9 String) +(declare-const Str10 String) +(declare-const Str11 String) +(declare-const Str12 String) +(declare-const Str13 String) +(declare-const Str14 String) +(declare-const Str15 String) +(declare-const Str16 String) +(declare-const Str17 String) +(declare-const Str18 String) +(declare-const Str19 String) +(assert (str.in_re Str19(re.opt (str.to_re Str10)))) +(assert (str.in_re Str9(re.opt (str.to_re Str18)))) +(assert (str.in_re (str.replace Str12 "jkngjj" Str14)(re.opt (str.to_re (str.++ Str13 "spifluyxzmbznnejkmfajdisgnyfeogvtwxuclzmrlmjmmwhly" Str5 Str19 "rsjusudbyjoyfpwbpasemhhxoayzouhoaekszsvhbsmnysbcih"))))) +(assert (str.in_re Str13(re.opt (str.to_re Str3)))) +(push 1) +(assert (str.in_re (str.++ Str12 (str.++ Str5 Str16 Str13) (str.++ Str5 "tqckdn" "hvhftx" (str.replace Str12 "jkngjj" Str14)) "trcuij" "ovnscketrkugxyqewkvuvondgahkfzwczexnyiziwhyqlomqie")(re.opt (str.to_re Str8)))) +(push 1) +(assert (str.in_re (str.++ Str13 (str.++ Str5 Str16 Str13))(re.++ (str.to_re (str.++ Str5 Str16 Str13)) (str.to_re "cjyfqapanogtdznjbtqlfrmmfauwjdpvnhfpfhzsxaarlfvlvs" )))) +(set-info :status sat) +(check-sat) |