From da61fb67d52a7d3ca4341739e966acbe93682c6a Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Wed, 23 Jan 2019 12:21:31 +0000 Subject: [PATCH 1/4] Add smt2_strings test suite directory --- regression/CMakeLists.txt | 1 + regression/Makefile | 1 + regression/smt2_strings/CMakeLists.txt | 3 +++ regression/smt2_strings/Makefile | 18 ++++++++++++++++++ 4 files changed, 23 insertions(+) create mode 100644 regression/smt2_strings/CMakeLists.txt create mode 100644 regression/smt2_strings/Makefile diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index c7508f6d470..504487fa939 100644 --- a/regression/CMakeLists.txt +++ b/regression/CMakeLists.txt @@ -32,6 +32,7 @@ add_subdirectory(cpp) add_subdirectory(cbmc-cover) add_subdirectory(goto-instrument-typedef) add_subdirectory(smt2_solver) +add_subdirectory(smt2_strings) add_subdirectory(strings) add_subdirectory(invariants) add_subdirectory(goto-diff) diff --git a/regression/Makefile b/regression/Makefile index 621e4a8402d..7711fc2e71f 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -10,6 +10,7 @@ DIRS = cbmc \ cbmc-cover \ goto-instrument-typedef \ smt2_solver \ + smt2_strings \ strings \ invariants \ goto-diff \ diff --git a/regression/smt2_strings/CMakeLists.txt b/regression/smt2_strings/CMakeLists.txt new file mode 100644 index 00000000000..5a4bad9c15d --- /dev/null +++ b/regression/smt2_strings/CMakeLists.txt @@ -0,0 +1,3 @@ +add_test_pl_tests( + "$" +) diff --git a/regression/smt2_strings/Makefile b/regression/smt2_strings/Makefile new file mode 100644 index 00000000000..3be14ea765c --- /dev/null +++ b/regression/smt2_strings/Makefile @@ -0,0 +1,18 @@ +default: tests.log + +test: + @../test.pl -p -c ../../../src/solvers/smt2_solver + +tests.log: ../test.pl + @../test.pl -p -c ../../../src/solvers/smt2_solver + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.c" "$$dir/*.out"; \ + fi; \ + done; + +clean: + find -name '*.out' -execdir $(RM) '{}' \; + $(RM) tests.log From 28c919258d1c0cdd63a9014e41caa98f6091e776 Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Wed, 23 Jan 2019 17:52:46 +0000 Subject: [PATCH 2/4] gitignore --- regression/smt2_strings/.gitignore | 1 + 1 file changed, 1 insertion(+) create mode 100644 regression/smt2_strings/.gitignore diff --git a/regression/smt2_strings/.gitignore b/regression/smt2_strings/.gitignore new file mode 100644 index 00000000000..353523cd8fb --- /dev/null +++ b/regression/smt2_strings/.gitignore @@ -0,0 +1 @@ +!*.smt2 From ce6e9b021d7f22c47304d7ef057f9231d32e784e Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Thu, 31 Jan 2019 09:56:33 +0000 Subject: [PATCH 3/4] Add README.md to smt2_strings --- regression/smt2_strings/README.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 regression/smt2_strings/README.md diff --git a/regression/smt2_strings/README.md b/regression/smt2_strings/README.md new file mode 100644 index 00000000000..18afac444f3 --- /dev/null +++ b/regression/smt2_strings/README.md @@ -0,0 +1,14 @@ +Test Suite for SMT2 String Operations +===================================== + +The purpose of this suite is to test the level of string support of cbmc's smt2 +backend. + +It can also be used to test the level of string support of any smt2 solver, by +using a command such as: +``` +../test.pl -p -F -c +``` + +(note the `-F` option to consider all tests tagged as "FUTURE"). + From 361050fde914624d8fa1c7f592345767b2c635b8 Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Wed, 23 Jan 2019 12:22:03 +0000 Subject: [PATCH 4/4] Add FUTURE tests for SMT2 string operations --- .../smt2_strings/concat_const_sat/concat_const_sat.desc | 8 ++++++++ .../smt2_strings/concat_const_sat/concat_const_sat.smt2 | 2 ++ .../concat_const_unsat/concat_const_unsat.desc | 8 ++++++++ .../concat_const_unsat/concat_const_unsat.smt2 | 2 ++ .../contains_const_sat/contains_const_sat.desc | 8 ++++++++ .../contains_const_sat/contains_const_sat.smt2 | 2 ++ .../contains_const_unsat/contains_const_unsat.desc | 8 ++++++++ .../contains_const_unsat/contains_const_unsat.smt2 | 2 ++ .../smt2_strings/indexof_const_sat/indexof_const_sat.desc | 8 ++++++++ .../smt2_strings/indexof_const_sat/indexof_const_sat.smt2 | 2 ++ .../indexof_const_unsat/indexof_const_unsat.desc | 8 ++++++++ .../indexof_const_unsat/indexof_const_unsat.smt2 | 2 ++ .../int_to_str_const_sat/int_to_str_const_sat.desc | 8 ++++++++ .../int_to_str_const_sat/int_to_str_const_sat.smt2 | 2 ++ .../int_to_str_const_unsat/int_to_str_const_unsat.desc | 8 ++++++++ .../int_to_str_const_unsat/int_to_str_const_unsat.smt2 | 2 ++ .../smt2_strings/length_const_sat/length_const_sat.desc | 8 ++++++++ .../smt2_strings/length_const_sat/length_const_sat.smt2 | 2 ++ .../length_const_unsat/length_const_unsat.desc | 8 ++++++++ .../length_const_unsat/length_const_unsat.smt2 | 2 ++ .../lex_order_const_sat/lex_order_const_sat.desc | 8 ++++++++ .../lex_order_const_sat/lex_order_const_sat.smt2 | 2 ++ .../lex_order_const_unsat/lex_order_const_unsat.desc | 8 ++++++++ .../lex_order_const_unsat/lex_order_const_unsat.smt2 | 2 ++ .../prefixof_const_sat/prefixof_const_sat.desc | 8 ++++++++ .../prefixof_const_sat/prefixof_const_sat.smt2 | 2 ++ .../prefixof_const_unsat/prefixof_const_unsat.desc | 8 ++++++++ .../prefixof_const_unsat/prefixof_const_unsat.smt2 | 2 ++ .../reflexive_lex_order_const_sat.desc | 8 ++++++++ .../reflexive_lex_order_const_sat.smt2 | 2 ++ .../reflexive_lex_order_const_sat2.desc | 8 ++++++++ .../reflexive_lex_order_const_sat2.smt2 | 2 ++ .../reflexive_lex_order_const_unsat.desc | 8 ++++++++ .../reflexive_lex_order_const_unsat.smt2 | 2 ++ .../regexp_all_const_sat/regexp_all_const_sat.desc | 8 ++++++++ .../regexp_all_const_sat/regexp_all_const_sat.smt2 | 2 ++ .../regexp_allchar_const_sat.desc | 8 ++++++++ .../regexp_allchar_const_sat.smt2 | 2 ++ .../regexp_allchar_const_unsat.desc | 8 ++++++++ .../regexp_allchar_const_unsat.smt2 | 2 ++ .../regexp_concat_const_sat/regexp_concat_const_sat.desc | 8 ++++++++ .../regexp_concat_const_sat/regexp_concat_const_sat.smt2 | 2 ++ .../regexp_concat_const_unsat.desc | 8 ++++++++ .../regexp_concat_const_unsat.smt2 | 2 ++ .../regexp_inter_const_sat/regexp_inter_const_sat.desc | 8 ++++++++ .../regexp_inter_const_sat/regexp_inter_const_sat.smt2 | 2 ++ .../regexp_inter_const_unsat.desc | 8 ++++++++ .../regexp_inter_const_unsat.smt2 | 2 ++ .../regexp_loop_const_sat/regexp_loop_const_sat.desc | 8 ++++++++ .../regexp_loop_const_sat/regexp_loop_const_sat.smt2 | 2 ++ .../regexp_loop_const_unsat/regexp_loop_const_unsat.desc | 8 ++++++++ .../regexp_loop_const_unsat/regexp_loop_const_unsat.smt2 | 2 ++ .../regexp_nostr_const_unsat.desc | 8 ++++++++ .../regexp_nostr_const_unsat.smt2 | 2 ++ .../regexp_opt_const_sat/regexp_opt_const_sat.desc | 8 ++++++++ .../regexp_opt_const_sat/regexp_opt_const_sat.smt2 | 2 ++ .../regexp_opt_const_sat/regexp_opt_const_sat2.desc | 8 ++++++++ .../regexp_opt_const_sat/regexp_opt_const_sat2.smt2 | 2 ++ .../regexp_opt_const_unsat/regexp_opt_const_unsat.desc | 8 ++++++++ .../regexp_opt_const_unsat/regexp_opt_const_unsat.smt2 | 2 ++ .../regexp_plus_const_sat/regexp_plus_const_sat.desc | 8 ++++++++ .../regexp_plus_const_sat/regexp_plus_const_sat.smt2 | 2 ++ .../regexp_plus_const_unsat/regexp_plus_const_unsat.desc | 8 ++++++++ .../regexp_plus_const_unsat/regexp_plus_const_unsat.smt2 | 2 ++ .../regexp_range_const_sat/regexp_range_const_sat.desc | 8 ++++++++ .../regexp_range_const_sat/regexp_range_const_sat.smt2 | 2 ++ .../regexp_range_const_unsat.desc | 8 ++++++++ .../regexp_range_const_unsat.smt2 | 2 ++ .../regexp_star_const_sat/regexp_star_const_sat.desc | 8 ++++++++ .../regexp_star_const_sat/regexp_star_const_sat.smt2 | 2 ++ .../regexp_star_const_unsat/regexp_star_const_unsat.desc | 8 ++++++++ .../regexp_star_const_unsat/regexp_star_const_unsat.smt2 | 2 ++ .../regexp_union_const_sat/regexp_union_const_sat.desc | 8 ++++++++ .../regexp_union_const_sat/regexp_union_const_sat.smt2 | 2 ++ .../regexp_union_const_unsat.desc | 8 ++++++++ .../regexp_union_const_unsat.smt2 | 2 ++ .../replace_all_const_sat/replace_all_const_sat.desc | 8 ++++++++ .../replace_all_const_sat/replace_all_const_sat.smt2 | 2 ++ .../replace_all_const_unsat/replace_all_const_unsat.desc | 8 ++++++++ .../replace_all_const_unsat/replace_all_const_unsat.smt2 | 2 ++ .../smt2_strings/replace_const_sat/replace_const_sat.desc | 8 ++++++++ .../smt2_strings/replace_const_sat/replace_const_sat.smt2 | 2 ++ .../replace_const_unsat/replace_const_unsat.desc | 8 ++++++++ .../replace_const_unsat/replace_const_unsat.smt2 | 2 ++ .../smt2_strings/str_at_const_sat/str_at_const_sat.desc | 8 ++++++++ .../smt2_strings/str_at_const_sat/str_at_const_sat.smt2 | 2 ++ .../str_at_const_unsat/str_at_const_unsat.desc | 8 ++++++++ .../str_at_const_unsat/str_at_const_unsat.smt2 | 2 ++ .../str_in_re_const_sat/str_in_re_const_sat.desc | 8 ++++++++ .../str_in_re_const_sat/str_in_re_const_sat.smt2 | 2 ++ .../str_in_re_const_unsat/str_in_re_const_unsat.desc | 8 ++++++++ .../str_in_re_const_unsat/str_in_re_const_unsat.smt2 | 2 ++ .../str_to_int_const_sat/str_to_int_const_sat.desc | 8 ++++++++ .../str_to_int_const_sat/str_to_int_const_sat.smt2 | 2 ++ .../str_to_int_const_unsat/str_to_int_const_unsat.desc | 8 ++++++++ .../str_to_int_const_unsat/str_to_int_const_unsat.smt2 | 2 ++ .../str_to_re_const_sat/str_to_re_const_sat.desc | 8 ++++++++ .../str_to_re_const_sat/str_to_re_const_sat.smt2 | 2 ++ .../str_to_re_const_unsat/str_to_re_const_unsat.desc | 8 ++++++++ .../str_to_re_const_unsat/str_to_re_const_unsat.smt2 | 2 ++ .../smt2_strings/substr_const_sat/substr_const_sat.desc | 8 ++++++++ .../smt2_strings/substr_const_sat/substr_const_sat.smt2 | 2 ++ .../substr_const_unsat/substr_const_unsat.desc | 8 ++++++++ .../substr_const_unsat/substr_const_unsat.smt2 | 2 ++ .../suffixof_const_sat/suffixof_const_sat.desc | 8 ++++++++ .../suffixof_const_sat/suffixof_const_sat.smt2 | 2 ++ .../suffixof_const_unsat/suffixof_const_unsat.desc | 8 ++++++++ .../suffixof_const_unsat/suffixof_const_unsat.smt2 | 2 ++ 108 files changed, 540 insertions(+) create mode 100644 regression/smt2_strings/concat_const_sat/concat_const_sat.desc create mode 100644 regression/smt2_strings/concat_const_sat/concat_const_sat.smt2 create mode 100644 regression/smt2_strings/concat_const_unsat/concat_const_unsat.desc create mode 100644 regression/smt2_strings/concat_const_unsat/concat_const_unsat.smt2 create mode 100644 regression/smt2_strings/contains_const_sat/contains_const_sat.desc create mode 100644 regression/smt2_strings/contains_const_sat/contains_const_sat.smt2 create mode 100644 regression/smt2_strings/contains_const_unsat/contains_const_unsat.desc create mode 100644 regression/smt2_strings/contains_const_unsat/contains_const_unsat.smt2 create mode 100644 regression/smt2_strings/indexof_const_sat/indexof_const_sat.desc create mode 100644 regression/smt2_strings/indexof_const_sat/indexof_const_sat.smt2 create mode 100644 regression/smt2_strings/indexof_const_unsat/indexof_const_unsat.desc create mode 100644 regression/smt2_strings/indexof_const_unsat/indexof_const_unsat.smt2 create mode 100644 regression/smt2_strings/int_to_str_const_sat/int_to_str_const_sat.desc create mode 100644 regression/smt2_strings/int_to_str_const_sat/int_to_str_const_sat.smt2 create mode 100644 regression/smt2_strings/int_to_str_const_unsat/int_to_str_const_unsat.desc create mode 100644 regression/smt2_strings/int_to_str_const_unsat/int_to_str_const_unsat.smt2 create mode 100644 regression/smt2_strings/length_const_sat/length_const_sat.desc create mode 100644 regression/smt2_strings/length_const_sat/length_const_sat.smt2 create mode 100644 regression/smt2_strings/length_const_unsat/length_const_unsat.desc create mode 100644 regression/smt2_strings/length_const_unsat/length_const_unsat.smt2 create mode 100644 regression/smt2_strings/lex_order_const_sat/lex_order_const_sat.desc create mode 100644 regression/smt2_strings/lex_order_const_sat/lex_order_const_sat.smt2 create mode 100644 regression/smt2_strings/lex_order_const_unsat/lex_order_const_unsat.desc create mode 100644 regression/smt2_strings/lex_order_const_unsat/lex_order_const_unsat.smt2 create mode 100644 regression/smt2_strings/prefixof_const_sat/prefixof_const_sat.desc create mode 100644 regression/smt2_strings/prefixof_const_sat/prefixof_const_sat.smt2 create mode 100644 regression/smt2_strings/prefixof_const_unsat/prefixof_const_unsat.desc create mode 100644 regression/smt2_strings/prefixof_const_unsat/prefixof_const_unsat.smt2 create mode 100644 regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat.desc create mode 100644 regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat.smt2 create mode 100644 regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat2.desc create mode 100644 regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat2.smt2 create mode 100644 regression/smt2_strings/reflexive_lex_order_const_unsat/reflexive_lex_order_const_unsat.desc create mode 100644 regression/smt2_strings/reflexive_lex_order_const_unsat/reflexive_lex_order_const_unsat.smt2 create mode 100644 regression/smt2_strings/regexp_all_const_sat/regexp_all_const_sat.desc create mode 100644 regression/smt2_strings/regexp_all_const_sat/regexp_all_const_sat.smt2 create mode 100644 regression/smt2_strings/regexp_allchar_const_sat/regexp_allchar_const_sat.desc create mode 100644 regression/smt2_strings/regexp_allchar_const_sat/regexp_allchar_const_sat.smt2 create mode 100644 regression/smt2_strings/regexp_allchar_const_unsat/regexp_allchar_const_unsat.desc create mode 100644 regression/smt2_strings/regexp_allchar_const_unsat/regexp_allchar_const_unsat.smt2 create mode 100644 regression/smt2_strings/regexp_concat_const_sat/regexp_concat_const_sat.desc create mode 100644 regression/smt2_strings/regexp_concat_const_sat/regexp_concat_const_sat.smt2 create mode 100644 regression/smt2_strings/regexp_concat_const_unsat/regexp_concat_const_unsat.desc create mode 100644 regression/smt2_strings/regexp_concat_const_unsat/regexp_concat_const_unsat.smt2 create mode 100644 regression/smt2_strings/regexp_inter_const_sat/regexp_inter_const_sat.desc create mode 100644 regression/smt2_strings/regexp_inter_const_sat/regexp_inter_const_sat.smt2 create mode 100644 regression/smt2_strings/regexp_inter_const_unsat/regexp_inter_const_unsat.desc create mode 100644 regression/smt2_strings/regexp_inter_const_unsat/regexp_inter_const_unsat.smt2 create mode 100644 regression/smt2_strings/regexp_loop_const_sat/regexp_loop_const_sat.desc create mode 100644 regression/smt2_strings/regexp_loop_const_sat/regexp_loop_const_sat.smt2 create mode 100644 regression/smt2_strings/regexp_loop_const_unsat/regexp_loop_const_unsat.desc create mode 100644 regression/smt2_strings/regexp_loop_const_unsat/regexp_loop_const_unsat.smt2 create mode 100644 regression/smt2_strings/regexp_nostr_const_unsat/regexp_nostr_const_unsat.desc create mode 100644 regression/smt2_strings/regexp_nostr_const_unsat/regexp_nostr_const_unsat.smt2 create mode 100644 regression/smt2_strings/regexp_opt_const_sat/regexp_opt_const_sat.desc create mode 100644 regression/smt2_strings/regexp_opt_const_sat/regexp_opt_const_sat.smt2 create mode 100644 regression/smt2_strings/regexp_opt_const_sat/regexp_opt_const_sat2.desc create mode 100644 regression/smt2_strings/regexp_opt_const_sat/regexp_opt_const_sat2.smt2 create mode 100644 regression/smt2_strings/regexp_opt_const_unsat/regexp_opt_const_unsat.desc create mode 100644 regression/smt2_strings/regexp_opt_const_unsat/regexp_opt_const_unsat.smt2 create mode 100644 regression/smt2_strings/regexp_plus_const_sat/regexp_plus_const_sat.desc create mode 100644 regression/smt2_strings/regexp_plus_const_sat/regexp_plus_const_sat.smt2 create mode 100644 regression/smt2_strings/regexp_plus_const_unsat/regexp_plus_const_unsat.desc create mode 100644 regression/smt2_strings/regexp_plus_const_unsat/regexp_plus_const_unsat.smt2 create mode 100644 regression/smt2_strings/regexp_range_const_sat/regexp_range_const_sat.desc create mode 100644 regression/smt2_strings/regexp_range_const_sat/regexp_range_const_sat.smt2 create mode 100644 regression/smt2_strings/regexp_range_const_unsat/regexp_range_const_unsat.desc create mode 100644 regression/smt2_strings/regexp_range_const_unsat/regexp_range_const_unsat.smt2 create mode 100644 regression/smt2_strings/regexp_star_const_sat/regexp_star_const_sat.desc create mode 100644 regression/smt2_strings/regexp_star_const_sat/regexp_star_const_sat.smt2 create mode 100644 regression/smt2_strings/regexp_star_const_unsat/regexp_star_const_unsat.desc create mode 100644 regression/smt2_strings/regexp_star_const_unsat/regexp_star_const_unsat.smt2 create mode 100644 regression/smt2_strings/regexp_union_const_sat/regexp_union_const_sat.desc create mode 100644 regression/smt2_strings/regexp_union_const_sat/regexp_union_const_sat.smt2 create mode 100644 regression/smt2_strings/regexp_union_const_unsat/regexp_union_const_unsat.desc create mode 100644 regression/smt2_strings/regexp_union_const_unsat/regexp_union_const_unsat.smt2 create mode 100644 regression/smt2_strings/replace_all_const_sat/replace_all_const_sat.desc create mode 100644 regression/smt2_strings/replace_all_const_sat/replace_all_const_sat.smt2 create mode 100644 regression/smt2_strings/replace_all_const_unsat/replace_all_const_unsat.desc create mode 100644 regression/smt2_strings/replace_all_const_unsat/replace_all_const_unsat.smt2 create mode 100644 regression/smt2_strings/replace_const_sat/replace_const_sat.desc create mode 100644 regression/smt2_strings/replace_const_sat/replace_const_sat.smt2 create mode 100644 regression/smt2_strings/replace_const_unsat/replace_const_unsat.desc create mode 100644 regression/smt2_strings/replace_const_unsat/replace_const_unsat.smt2 create mode 100644 regression/smt2_strings/str_at_const_sat/str_at_const_sat.desc create mode 100644 regression/smt2_strings/str_at_const_sat/str_at_const_sat.smt2 create mode 100644 regression/smt2_strings/str_at_const_unsat/str_at_const_unsat.desc create mode 100644 regression/smt2_strings/str_at_const_unsat/str_at_const_unsat.smt2 create mode 100644 regression/smt2_strings/str_in_re_const_sat/str_in_re_const_sat.desc create mode 100644 regression/smt2_strings/str_in_re_const_sat/str_in_re_const_sat.smt2 create mode 100644 regression/smt2_strings/str_in_re_const_unsat/str_in_re_const_unsat.desc create mode 100644 regression/smt2_strings/str_in_re_const_unsat/str_in_re_const_unsat.smt2 create mode 100644 regression/smt2_strings/str_to_int_const_sat/str_to_int_const_sat.desc create mode 100644 regression/smt2_strings/str_to_int_const_sat/str_to_int_const_sat.smt2 create mode 100644 regression/smt2_strings/str_to_int_const_unsat/str_to_int_const_unsat.desc create mode 100644 regression/smt2_strings/str_to_int_const_unsat/str_to_int_const_unsat.smt2 create mode 100644 regression/smt2_strings/str_to_re_const_sat/str_to_re_const_sat.desc create mode 100644 regression/smt2_strings/str_to_re_const_sat/str_to_re_const_sat.smt2 create mode 100644 regression/smt2_strings/str_to_re_const_unsat/str_to_re_const_unsat.desc create mode 100644 regression/smt2_strings/str_to_re_const_unsat/str_to_re_const_unsat.smt2 create mode 100644 regression/smt2_strings/substr_const_sat/substr_const_sat.desc create mode 100644 regression/smt2_strings/substr_const_sat/substr_const_sat.smt2 create mode 100644 regression/smt2_strings/substr_const_unsat/substr_const_unsat.desc create mode 100644 regression/smt2_strings/substr_const_unsat/substr_const_unsat.smt2 create mode 100644 regression/smt2_strings/suffixof_const_sat/suffixof_const_sat.desc create mode 100644 regression/smt2_strings/suffixof_const_sat/suffixof_const_sat.smt2 create mode 100644 regression/smt2_strings/suffixof_const_unsat/suffixof_const_unsat.desc create mode 100644 regression/smt2_strings/suffixof_const_unsat/suffixof_const_unsat.smt2 diff --git a/regression/smt2_strings/concat_const_sat/concat_const_sat.desc b/regression/smt2_strings/concat_const_sat/concat_const_sat.desc new file mode 100644 index 00000000000..42dba0e50a4 --- /dev/null +++ b/regression/smt2_strings/concat_const_sat/concat_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +concat_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/concat_const_sat/concat_const_sat.smt2 b/regression/smt2_strings/concat_const_sat/concat_const_sat.smt2 new file mode 100644 index 00000000000..444253587fe --- /dev/null +++ b/regression/smt2_strings/concat_const_sat/concat_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (= (str.++ "abc" "def" "" "gh") "abcdefgh")) +(check-sat) diff --git a/regression/smt2_strings/concat_const_unsat/concat_const_unsat.desc b/regression/smt2_strings/concat_const_unsat/concat_const_unsat.desc new file mode 100644 index 00000000000..1a360d2833a --- /dev/null +++ b/regression/smt2_strings/concat_const_unsat/concat_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +concat_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/concat_const_unsat/concat_const_unsat.smt2 b/regression/smt2_strings/concat_const_unsat/concat_const_unsat.smt2 new file mode 100644 index 00000000000..aea2cfe04e1 --- /dev/null +++ b/regression/smt2_strings/concat_const_unsat/concat_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (= (str.++ "abc" "cdef") "abcde")) +(check-sat) diff --git a/regression/smt2_strings/contains_const_sat/contains_const_sat.desc b/regression/smt2_strings/contains_const_sat/contains_const_sat.desc new file mode 100644 index 00000000000..c01aeb79927 --- /dev/null +++ b/regression/smt2_strings/contains_const_sat/contains_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +contains_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/contains_const_sat/contains_const_sat.smt2 b/regression/smt2_strings/contains_const_sat/contains_const_sat.smt2 new file mode 100644 index 00000000000..5f0b30ea8b3 --- /dev/null +++ b/regression/smt2_strings/contains_const_sat/contains_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (str.contains "abcdef" "bcd")) +(check-sat) diff --git a/regression/smt2_strings/contains_const_unsat/contains_const_unsat.desc b/regression/smt2_strings/contains_const_unsat/contains_const_unsat.desc new file mode 100644 index 00000000000..dc0f8909ba9 --- /dev/null +++ b/regression/smt2_strings/contains_const_unsat/contains_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +contains_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/contains_const_unsat/contains_const_unsat.smt2 b/regression/smt2_strings/contains_const_unsat/contains_const_unsat.smt2 new file mode 100644 index 00000000000..0b6082f62c5 --- /dev/null +++ b/regression/smt2_strings/contains_const_unsat/contains_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (str.contains "abcdef" "dc")) +(check-sat) diff --git a/regression/smt2_strings/indexof_const_sat/indexof_const_sat.desc b/regression/smt2_strings/indexof_const_sat/indexof_const_sat.desc new file mode 100644 index 00000000000..8d818ffabe4 --- /dev/null +++ b/regression/smt2_strings/indexof_const_sat/indexof_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +indexof_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/indexof_const_sat/indexof_const_sat.smt2 b/regression/smt2_strings/indexof_const_sat/indexof_const_sat.smt2 new file mode 100644 index 00000000000..6f7fcfec66f --- /dev/null +++ b/regression/smt2_strings/indexof_const_sat/indexof_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (= (str.indexof "abcdef" "cde" 1) 2)) +(check-sat) diff --git a/regression/smt2_strings/indexof_const_unsat/indexof_const_unsat.desc b/regression/smt2_strings/indexof_const_unsat/indexof_const_unsat.desc new file mode 100644 index 00000000000..ab1b8be3982 --- /dev/null +++ b/regression/smt2_strings/indexof_const_unsat/indexof_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +indexof_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/indexof_const_unsat/indexof_const_unsat.smt2 b/regression/smt2_strings/indexof_const_unsat/indexof_const_unsat.smt2 new file mode 100644 index 00000000000..7131ad22950 --- /dev/null +++ b/regression/smt2_strings/indexof_const_unsat/indexof_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (= (str.indexof "abcdef" "cde" 1) 1)) +(check-sat) diff --git a/regression/smt2_strings/int_to_str_const_sat/int_to_str_const_sat.desc b/regression/smt2_strings/int_to_str_const_sat/int_to_str_const_sat.desc new file mode 100644 index 00000000000..168f574d6c0 --- /dev/null +++ b/regression/smt2_strings/int_to_str_const_sat/int_to_str_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +int_to_str_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/int_to_str_const_sat/int_to_str_const_sat.smt2 b/regression/smt2_strings/int_to_str_const_sat/int_to_str_const_sat.smt2 new file mode 100644 index 00000000000..af9cf15b322 --- /dev/null +++ b/regression/smt2_strings/int_to_str_const_sat/int_to_str_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (= (int.to.str 1234567890) "1234567890")) +(check-sat) diff --git a/regression/smt2_strings/int_to_str_const_unsat/int_to_str_const_unsat.desc b/regression/smt2_strings/int_to_str_const_unsat/int_to_str_const_unsat.desc new file mode 100644 index 00000000000..7df7ce1148b --- /dev/null +++ b/regression/smt2_strings/int_to_str_const_unsat/int_to_str_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +int_to_str_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/int_to_str_const_unsat/int_to_str_const_unsat.smt2 b/regression/smt2_strings/int_to_str_const_unsat/int_to_str_const_unsat.smt2 new file mode 100644 index 00000000000..2827019c645 --- /dev/null +++ b/regression/smt2_strings/int_to_str_const_unsat/int_to_str_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (= (int.to.str 1234567890) "1234467890")) +(check-sat) diff --git a/regression/smt2_strings/length_const_sat/length_const_sat.desc b/regression/smt2_strings/length_const_sat/length_const_sat.desc new file mode 100644 index 00000000000..f72f9eed977 --- /dev/null +++ b/regression/smt2_strings/length_const_sat/length_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +length_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/length_const_sat/length_const_sat.smt2 b/regression/smt2_strings/length_const_sat/length_const_sat.smt2 new file mode 100644 index 00000000000..aef1ce7a64a --- /dev/null +++ b/regression/smt2_strings/length_const_sat/length_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (= (str.len "abc") 3)) +(check-sat) diff --git a/regression/smt2_strings/length_const_unsat/length_const_unsat.desc b/regression/smt2_strings/length_const_unsat/length_const_unsat.desc new file mode 100644 index 00000000000..4e6629e6f10 --- /dev/null +++ b/regression/smt2_strings/length_const_unsat/length_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +length_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/length_const_unsat/length_const_unsat.smt2 b/regression/smt2_strings/length_const_unsat/length_const_unsat.smt2 new file mode 100644 index 00000000000..eab1273dfac --- /dev/null +++ b/regression/smt2_strings/length_const_unsat/length_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (= (str.len "abc") 4)) +(check-sat) diff --git a/regression/smt2_strings/lex_order_const_sat/lex_order_const_sat.desc b/regression/smt2_strings/lex_order_const_sat/lex_order_const_sat.desc new file mode 100644 index 00000000000..292fa9cf69b --- /dev/null +++ b/regression/smt2_strings/lex_order_const_sat/lex_order_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +lex_order_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/lex_order_const_sat/lex_order_const_sat.smt2 b/regression/smt2_strings/lex_order_const_sat/lex_order_const_sat.smt2 new file mode 100644 index 00000000000..601b3e20c72 --- /dev/null +++ b/regression/smt2_strings/lex_order_const_sat/lex_order_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (str.< "abc" "acc")) +(check-sat) diff --git a/regression/smt2_strings/lex_order_const_unsat/lex_order_const_unsat.desc b/regression/smt2_strings/lex_order_const_unsat/lex_order_const_unsat.desc new file mode 100644 index 00000000000..2d26a665b6f --- /dev/null +++ b/regression/smt2_strings/lex_order_const_unsat/lex_order_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +lex_order_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/lex_order_const_unsat/lex_order_const_unsat.smt2 b/regression/smt2_strings/lex_order_const_unsat/lex_order_const_unsat.smt2 new file mode 100644 index 00000000000..f6668edf73d --- /dev/null +++ b/regression/smt2_strings/lex_order_const_unsat/lex_order_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (str.< "abc" "aac")) +(check-sat) diff --git a/regression/smt2_strings/prefixof_const_sat/prefixof_const_sat.desc b/regression/smt2_strings/prefixof_const_sat/prefixof_const_sat.desc new file mode 100644 index 00000000000..25648087e51 --- /dev/null +++ b/regression/smt2_strings/prefixof_const_sat/prefixof_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +prefixof_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/prefixof_const_sat/prefixof_const_sat.smt2 b/regression/smt2_strings/prefixof_const_sat/prefixof_const_sat.smt2 new file mode 100644 index 00000000000..ff111d32e9e --- /dev/null +++ b/regression/smt2_strings/prefixof_const_sat/prefixof_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (str.prefixof "abc" "abcdef")) +(check-sat) diff --git a/regression/smt2_strings/prefixof_const_unsat/prefixof_const_unsat.desc b/regression/smt2_strings/prefixof_const_unsat/prefixof_const_unsat.desc new file mode 100644 index 00000000000..2646c969069 --- /dev/null +++ b/regression/smt2_strings/prefixof_const_unsat/prefixof_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +prefixof_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/prefixof_const_unsat/prefixof_const_unsat.smt2 b/regression/smt2_strings/prefixof_const_unsat/prefixof_const_unsat.smt2 new file mode 100644 index 00000000000..0b213d6da06 --- /dev/null +++ b/regression/smt2_strings/prefixof_const_unsat/prefixof_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (str.prefixof "bc" "abcdef")) +(check-sat) diff --git a/regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat.desc b/regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat.desc new file mode 100644 index 00000000000..e8edec2152e --- /dev/null +++ b/regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +reflexive_lex_order_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat.smt2 b/regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat.smt2 new file mode 100644 index 00000000000..3c3d37909bd --- /dev/null +++ b/regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (str.<= "abc" "acc")) +(check-sat) diff --git a/regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat2.desc b/regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat2.desc new file mode 100644 index 00000000000..841b14c51cf --- /dev/null +++ b/regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat2.desc @@ -0,0 +1,8 @@ +FUTURE +reflexive_lex_order_const_sat2.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat2.smt2 b/regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat2.smt2 new file mode 100644 index 00000000000..e4c11edd78c --- /dev/null +++ b/regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat2.smt2 @@ -0,0 +1,2 @@ +(assert (str.<= "abc" "abc")) +(check-sat) diff --git a/regression/smt2_strings/reflexive_lex_order_const_unsat/reflexive_lex_order_const_unsat.desc b/regression/smt2_strings/reflexive_lex_order_const_unsat/reflexive_lex_order_const_unsat.desc new file mode 100644 index 00000000000..d529e827013 --- /dev/null +++ b/regression/smt2_strings/reflexive_lex_order_const_unsat/reflexive_lex_order_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +reflexive_lex_order_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/reflexive_lex_order_const_unsat/reflexive_lex_order_const_unsat.smt2 b/regression/smt2_strings/reflexive_lex_order_const_unsat/reflexive_lex_order_const_unsat.smt2 new file mode 100644 index 00000000000..6182e812984 --- /dev/null +++ b/regression/smt2_strings/reflexive_lex_order_const_unsat/reflexive_lex_order_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (str.<= "acc" "abc")) +(check-sat) diff --git a/regression/smt2_strings/regexp_all_const_sat/regexp_all_const_sat.desc b/regression/smt2_strings/regexp_all_const_sat/regexp_all_const_sat.desc new file mode 100644 index 00000000000..9ca2c8b51be --- /dev/null +++ b/regression/smt2_strings/regexp_all_const_sat/regexp_all_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +regexp_all_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/regexp_all_const_sat/regexp_all_const_sat.smt2 b/regression/smt2_strings/regexp_all_const_sat/regexp_all_const_sat.smt2 new file mode 100644 index 00000000000..f7d8cb9d3ec --- /dev/null +++ b/regression/smt2_strings/regexp_all_const_sat/regexp_all_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "abc" (re.* re.all))) +(check-sat) diff --git a/regression/smt2_strings/regexp_allchar_const_sat/regexp_allchar_const_sat.desc b/regression/smt2_strings/regexp_allchar_const_sat/regexp_allchar_const_sat.desc new file mode 100644 index 00000000000..16cb1db8a6e --- /dev/null +++ b/regression/smt2_strings/regexp_allchar_const_sat/regexp_allchar_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +regexp_allchar_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/regexp_allchar_const_sat/regexp_allchar_const_sat.smt2 b/regression/smt2_strings/regexp_allchar_const_sat/regexp_allchar_const_sat.smt2 new file mode 100644 index 00000000000..40230c9c107 --- /dev/null +++ b/regression/smt2_strings/regexp_allchar_const_sat/regexp_allchar_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "aaabbb" (re.++ (re.* (str.to.re "a")) (re.* re.allchar)))) +(check-sat) diff --git a/regression/smt2_strings/regexp_allchar_const_unsat/regexp_allchar_const_unsat.desc b/regression/smt2_strings/regexp_allchar_const_unsat/regexp_allchar_const_unsat.desc new file mode 100644 index 00000000000..0d5eba92ccf --- /dev/null +++ b/regression/smt2_strings/regexp_allchar_const_unsat/regexp_allchar_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +regexp_allchar_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/regexp_allchar_const_unsat/regexp_allchar_const_unsat.smt2 b/regression/smt2_strings/regexp_allchar_const_unsat/regexp_allchar_const_unsat.smt2 new file mode 100644 index 00000000000..c6ac0fcb8c8 --- /dev/null +++ b/regression/smt2_strings/regexp_allchar_const_unsat/regexp_allchar_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "a" (re.++ (re.+ (str.to.re "a")) (re.+ re.allchar)))) +(check-sat) diff --git a/regression/smt2_strings/regexp_concat_const_sat/regexp_concat_const_sat.desc b/regression/smt2_strings/regexp_concat_const_sat/regexp_concat_const_sat.desc new file mode 100644 index 00000000000..3e90f53d98f --- /dev/null +++ b/regression/smt2_strings/regexp_concat_const_sat/regexp_concat_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +regexp_concat_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/regexp_concat_const_sat/regexp_concat_const_sat.smt2 b/regression/smt2_strings/regexp_concat_const_sat/regexp_concat_const_sat.smt2 new file mode 100644 index 00000000000..5437ffcc24f --- /dev/null +++ b/regression/smt2_strings/regexp_concat_const_sat/regexp_concat_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "aaabbb" (re.++ (re.* (str.to.re "a")) (re.* (str.to.re "b"))))) +(check-sat) diff --git a/regression/smt2_strings/regexp_concat_const_unsat/regexp_concat_const_unsat.desc b/regression/smt2_strings/regexp_concat_const_unsat/regexp_concat_const_unsat.desc new file mode 100644 index 00000000000..c1a0d081d96 --- /dev/null +++ b/regression/smt2_strings/regexp_concat_const_unsat/regexp_concat_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +regexp_concat_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/regexp_concat_const_unsat/regexp_concat_const_unsat.smt2 b/regression/smt2_strings/regexp_concat_const_unsat/regexp_concat_const_unsat.smt2 new file mode 100644 index 00000000000..60df446a2d6 --- /dev/null +++ b/regression/smt2_strings/regexp_concat_const_unsat/regexp_concat_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "aaabbbc" (re.++ (re.* (str.to.re "a")) (re.* (str.to.re "b"))))) +(check-sat) diff --git a/regression/smt2_strings/regexp_inter_const_sat/regexp_inter_const_sat.desc b/regression/smt2_strings/regexp_inter_const_sat/regexp_inter_const_sat.desc new file mode 100644 index 00000000000..c19d13a6228 --- /dev/null +++ b/regression/smt2_strings/regexp_inter_const_sat/regexp_inter_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +regexp_inter_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/regexp_inter_const_sat/regexp_inter_const_sat.smt2 b/regression/smt2_strings/regexp_inter_const_sat/regexp_inter_const_sat.smt2 new file mode 100644 index 00000000000..54b67593e40 --- /dev/null +++ b/regression/smt2_strings/regexp_inter_const_sat/regexp_inter_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "e" (re.inter (re.range "a" "h") (re.range "d" "w")))) +(check-sat) diff --git a/regression/smt2_strings/regexp_inter_const_unsat/regexp_inter_const_unsat.desc b/regression/smt2_strings/regexp_inter_const_unsat/regexp_inter_const_unsat.desc new file mode 100644 index 00000000000..0a761e22d58 --- /dev/null +++ b/regression/smt2_strings/regexp_inter_const_unsat/regexp_inter_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +regexp_inter_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/regexp_inter_const_unsat/regexp_inter_const_unsat.smt2 b/regression/smt2_strings/regexp_inter_const_unsat/regexp_inter_const_unsat.smt2 new file mode 100644 index 00000000000..a29ab6609ba --- /dev/null +++ b/regression/smt2_strings/regexp_inter_const_unsat/regexp_inter_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "e" (re.inter (re.range "a" "b") (re.range "b" "w")))) +(check-sat) diff --git a/regression/smt2_strings/regexp_loop_const_sat/regexp_loop_const_sat.desc b/regression/smt2_strings/regexp_loop_const_sat/regexp_loop_const_sat.desc new file mode 100644 index 00000000000..1f392b09c5f --- /dev/null +++ b/regression/smt2_strings/regexp_loop_const_sat/regexp_loop_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +regexp_loop_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/regexp_loop_const_sat/regexp_loop_const_sat.smt2 b/regression/smt2_strings/regexp_loop_const_sat/regexp_loop_const_sat.smt2 new file mode 100644 index 00000000000..719d02e0e08 --- /dev/null +++ b/regression/smt2_strings/regexp_loop_const_sat/regexp_loop_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "aaa" ((_ re.loop 3 3) (str.to.re "a")))) +(check-sat) diff --git a/regression/smt2_strings/regexp_loop_const_unsat/regexp_loop_const_unsat.desc b/regression/smt2_strings/regexp_loop_const_unsat/regexp_loop_const_unsat.desc new file mode 100644 index 00000000000..c542ca386dc --- /dev/null +++ b/regression/smt2_strings/regexp_loop_const_unsat/regexp_loop_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +regexp_loop_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/regexp_loop_const_unsat/regexp_loop_const_unsat.smt2 b/regression/smt2_strings/regexp_loop_const_unsat/regexp_loop_const_unsat.smt2 new file mode 100644 index 00000000000..300453690f0 --- /dev/null +++ b/regression/smt2_strings/regexp_loop_const_unsat/regexp_loop_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "aaa" ((_ re.loop 1 2) (str.to.re "a")))) +(check-sat) diff --git a/regression/smt2_strings/regexp_nostr_const_unsat/regexp_nostr_const_unsat.desc b/regression/smt2_strings/regexp_nostr_const_unsat/regexp_nostr_const_unsat.desc new file mode 100644 index 00000000000..c4244112541 --- /dev/null +++ b/regression/smt2_strings/regexp_nostr_const_unsat/regexp_nostr_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +regexp_nostr_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/regexp_nostr_const_unsat/regexp_nostr_const_unsat.smt2 b/regression/smt2_strings/regexp_nostr_const_unsat/regexp_nostr_const_unsat.smt2 new file mode 100644 index 00000000000..f5f63c0482a --- /dev/null +++ b/regression/smt2_strings/regexp_nostr_const_unsat/regexp_nostr_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "a" re.nostr)) +(check-sat) diff --git a/regression/smt2_strings/regexp_opt_const_sat/regexp_opt_const_sat.desc b/regression/smt2_strings/regexp_opt_const_sat/regexp_opt_const_sat.desc new file mode 100644 index 00000000000..fed610801ee --- /dev/null +++ b/regression/smt2_strings/regexp_opt_const_sat/regexp_opt_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +regexp_opt_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/regexp_opt_const_sat/regexp_opt_const_sat.smt2 b/regression/smt2_strings/regexp_opt_const_sat/regexp_opt_const_sat.smt2 new file mode 100644 index 00000000000..d3d2286b699 --- /dev/null +++ b/regression/smt2_strings/regexp_opt_const_sat/regexp_opt_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "aaab" (re.++ (re.+ (str.to.re "a")) (re.opt (str.to.re "b"))))) +(check-sat) diff --git a/regression/smt2_strings/regexp_opt_const_sat/regexp_opt_const_sat2.desc b/regression/smt2_strings/regexp_opt_const_sat/regexp_opt_const_sat2.desc new file mode 100644 index 00000000000..64b937d0006 --- /dev/null +++ b/regression/smt2_strings/regexp_opt_const_sat/regexp_opt_const_sat2.desc @@ -0,0 +1,8 @@ +FUTURE +regexp_opt_const_sat2.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/regexp_opt_const_sat/regexp_opt_const_sat2.smt2 b/regression/smt2_strings/regexp_opt_const_sat/regexp_opt_const_sat2.smt2 new file mode 100644 index 00000000000..99b06c5ec61 --- /dev/null +++ b/regression/smt2_strings/regexp_opt_const_sat/regexp_opt_const_sat2.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "aaa" (re.++ (re.+ (str.to.re "a")) (re.opt (str.to.re "b"))))) +(check-sat) diff --git a/regression/smt2_strings/regexp_opt_const_unsat/regexp_opt_const_unsat.desc b/regression/smt2_strings/regexp_opt_const_unsat/regexp_opt_const_unsat.desc new file mode 100644 index 00000000000..d7f892dc0c7 --- /dev/null +++ b/regression/smt2_strings/regexp_opt_const_unsat/regexp_opt_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +regexp_opt_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/regexp_opt_const_unsat/regexp_opt_const_unsat.smt2 b/regression/smt2_strings/regexp_opt_const_unsat/regexp_opt_const_unsat.smt2 new file mode 100644 index 00000000000..0b34669a7d3 --- /dev/null +++ b/regression/smt2_strings/regexp_opt_const_unsat/regexp_opt_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "aaac" (re.++ (re.+ (str.to.re "a")) (re.opt (str.to.re "b"))))) +(check-sat) diff --git a/regression/smt2_strings/regexp_plus_const_sat/regexp_plus_const_sat.desc b/regression/smt2_strings/regexp_plus_const_sat/regexp_plus_const_sat.desc new file mode 100644 index 00000000000..d5d5f51e4e0 --- /dev/null +++ b/regression/smt2_strings/regexp_plus_const_sat/regexp_plus_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +regexp_plus_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/regexp_plus_const_sat/regexp_plus_const_sat.smt2 b/regression/smt2_strings/regexp_plus_const_sat/regexp_plus_const_sat.smt2 new file mode 100644 index 00000000000..0792a0e73b3 --- /dev/null +++ b/regression/smt2_strings/regexp_plus_const_sat/regexp_plus_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "aaabbb" (re.++ (re.+ (str.to.re "a")) (re.+ (str.to.re "b"))))) +(check-sat) diff --git a/regression/smt2_strings/regexp_plus_const_unsat/regexp_plus_const_unsat.desc b/regression/smt2_strings/regexp_plus_const_unsat/regexp_plus_const_unsat.desc new file mode 100644 index 00000000000..fff3a369aaa --- /dev/null +++ b/regression/smt2_strings/regexp_plus_const_unsat/regexp_plus_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +regexp_plus_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/regexp_plus_const_unsat/regexp_plus_const_unsat.smt2 b/regression/smt2_strings/regexp_plus_const_unsat/regexp_plus_const_unsat.smt2 new file mode 100644 index 00000000000..0586a94c9cd --- /dev/null +++ b/regression/smt2_strings/regexp_plus_const_unsat/regexp_plus_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "aaa" (re.++ (re.+ (str.to.re "a")) (re.+ (str.to.re "b"))))) +(check-sat) diff --git a/regression/smt2_strings/regexp_range_const_sat/regexp_range_const_sat.desc b/regression/smt2_strings/regexp_range_const_sat/regexp_range_const_sat.desc new file mode 100644 index 00000000000..41d0627752c --- /dev/null +++ b/regression/smt2_strings/regexp_range_const_sat/regexp_range_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +regexp_range_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/regexp_range_const_sat/regexp_range_const_sat.smt2 b/regression/smt2_strings/regexp_range_const_sat/regexp_range_const_sat.smt2 new file mode 100644 index 00000000000..726b216c30e --- /dev/null +++ b/regression/smt2_strings/regexp_range_const_sat/regexp_range_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "c" (re.range "a" "f"))) +(check-sat) diff --git a/regression/smt2_strings/regexp_range_const_unsat/regexp_range_const_unsat.desc b/regression/smt2_strings/regexp_range_const_unsat/regexp_range_const_unsat.desc new file mode 100644 index 00000000000..b38aae9f79f --- /dev/null +++ b/regression/smt2_strings/regexp_range_const_unsat/regexp_range_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +regexp_range_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/regexp_range_const_unsat/regexp_range_const_unsat.smt2 b/regression/smt2_strings/regexp_range_const_unsat/regexp_range_const_unsat.smt2 new file mode 100644 index 00000000000..c7ee89346a7 --- /dev/null +++ b/regression/smt2_strings/regexp_range_const_unsat/regexp_range_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "w" (re.range "a" "f"))) +(check-sat) diff --git a/regression/smt2_strings/regexp_star_const_sat/regexp_star_const_sat.desc b/regression/smt2_strings/regexp_star_const_sat/regexp_star_const_sat.desc new file mode 100644 index 00000000000..1e4fe253e7b --- /dev/null +++ b/regression/smt2_strings/regexp_star_const_sat/regexp_star_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +regexp_star_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/regexp_star_const_sat/regexp_star_const_sat.smt2 b/regression/smt2_strings/regexp_star_const_sat/regexp_star_const_sat.smt2 new file mode 100644 index 00000000000..5437ffcc24f --- /dev/null +++ b/regression/smt2_strings/regexp_star_const_sat/regexp_star_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "aaabbb" (re.++ (re.* (str.to.re "a")) (re.* (str.to.re "b"))))) +(check-sat) diff --git a/regression/smt2_strings/regexp_star_const_unsat/regexp_star_const_unsat.desc b/regression/smt2_strings/regexp_star_const_unsat/regexp_star_const_unsat.desc new file mode 100644 index 00000000000..b013f541918 --- /dev/null +++ b/regression/smt2_strings/regexp_star_const_unsat/regexp_star_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +regexp_star_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/regexp_star_const_unsat/regexp_star_const_unsat.smt2 b/regression/smt2_strings/regexp_star_const_unsat/regexp_star_const_unsat.smt2 new file mode 100644 index 00000000000..60df446a2d6 --- /dev/null +++ b/regression/smt2_strings/regexp_star_const_unsat/regexp_star_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "aaabbbc" (re.++ (re.* (str.to.re "a")) (re.* (str.to.re "b"))))) +(check-sat) diff --git a/regression/smt2_strings/regexp_union_const_sat/regexp_union_const_sat.desc b/regression/smt2_strings/regexp_union_const_sat/regexp_union_const_sat.desc new file mode 100644 index 00000000000..8da32c9b14e --- /dev/null +++ b/regression/smt2_strings/regexp_union_const_sat/regexp_union_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +regexp_union_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/regexp_union_const_sat/regexp_union_const_sat.smt2 b/regression/smt2_strings/regexp_union_const_sat/regexp_union_const_sat.smt2 new file mode 100644 index 00000000000..1e6f164e510 --- /dev/null +++ b/regression/smt2_strings/regexp_union_const_sat/regexp_union_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "ab" (re.union (str.to.re "ab") (str.to.re "cd")))) +(check-sat) diff --git a/regression/smt2_strings/regexp_union_const_unsat/regexp_union_const_unsat.desc b/regression/smt2_strings/regexp_union_const_unsat/regexp_union_const_unsat.desc new file mode 100644 index 00000000000..8b5e27dafe8 --- /dev/null +++ b/regression/smt2_strings/regexp_union_const_unsat/regexp_union_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +regexp_union_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/regexp_union_const_unsat/regexp_union_const_unsat.smt2 b/regression/smt2_strings/regexp_union_const_unsat/regexp_union_const_unsat.smt2 new file mode 100644 index 00000000000..f424f46db92 --- /dev/null +++ b/regression/smt2_strings/regexp_union_const_unsat/regexp_union_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "abcd" (re.union (str.to.re "ab") (str.to.re "cd")))) +(check-sat) diff --git a/regression/smt2_strings/replace_all_const_sat/replace_all_const_sat.desc b/regression/smt2_strings/replace_all_const_sat/replace_all_const_sat.desc new file mode 100644 index 00000000000..dbb6ba8d48a --- /dev/null +++ b/regression/smt2_strings/replace_all_const_sat/replace_all_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +replace_all_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/replace_all_const_sat/replace_all_const_sat.smt2 b/regression/smt2_strings/replace_all_const_sat/replace_all_const_sat.smt2 new file mode 100644 index 00000000000..19ecbcad9f7 --- /dev/null +++ b/regression/smt2_strings/replace_all_const_sat/replace_all_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (= (str.replaceall "abcdefabcdef" "bc" "xy") "axydefaxydef")) +(check-sat) diff --git a/regression/smt2_strings/replace_all_const_unsat/replace_all_const_unsat.desc b/regression/smt2_strings/replace_all_const_unsat/replace_all_const_unsat.desc new file mode 100644 index 00000000000..7f6bfff8b9b --- /dev/null +++ b/regression/smt2_strings/replace_all_const_unsat/replace_all_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +replace_all_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/replace_all_const_unsat/replace_all_const_unsat.smt2 b/regression/smt2_strings/replace_all_const_unsat/replace_all_const_unsat.smt2 new file mode 100644 index 00000000000..3f109bcca43 --- /dev/null +++ b/regression/smt2_strings/replace_all_const_unsat/replace_all_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (= (str.replaceall "abcdefabcdef" "bc" "xy") "axydefaibcdef")) +(check-sat) diff --git a/regression/smt2_strings/replace_const_sat/replace_const_sat.desc b/regression/smt2_strings/replace_const_sat/replace_const_sat.desc new file mode 100644 index 00000000000..9f5b9fef02c --- /dev/null +++ b/regression/smt2_strings/replace_const_sat/replace_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +replace_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/replace_const_sat/replace_const_sat.smt2 b/regression/smt2_strings/replace_const_sat/replace_const_sat.smt2 new file mode 100644 index 00000000000..f74d276fe2e --- /dev/null +++ b/regression/smt2_strings/replace_const_sat/replace_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (= (str.replace "abcdefabcdef" "bc" "xy") "axydefabcdef")) +(check-sat) diff --git a/regression/smt2_strings/replace_const_unsat/replace_const_unsat.desc b/regression/smt2_strings/replace_const_unsat/replace_const_unsat.desc new file mode 100644 index 00000000000..fa8e9be3d98 --- /dev/null +++ b/regression/smt2_strings/replace_const_unsat/replace_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +replace_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/replace_const_unsat/replace_const_unsat.smt2 b/regression/smt2_strings/replace_const_unsat/replace_const_unsat.smt2 new file mode 100644 index 00000000000..2ae20e861bc --- /dev/null +++ b/regression/smt2_strings/replace_const_unsat/replace_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (= (str.replace "abcdefabcdef" "bc" "xy") "abcdefabcdef")) +(check-sat) diff --git a/regression/smt2_strings/str_at_const_sat/str_at_const_sat.desc b/regression/smt2_strings/str_at_const_sat/str_at_const_sat.desc new file mode 100644 index 00000000000..8d47d7ec505 --- /dev/null +++ b/regression/smt2_strings/str_at_const_sat/str_at_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +str_at_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/str_at_const_sat/str_at_const_sat.smt2 b/regression/smt2_strings/str_at_const_sat/str_at_const_sat.smt2 new file mode 100644 index 00000000000..af6ea359cd5 --- /dev/null +++ b/regression/smt2_strings/str_at_const_sat/str_at_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (= (str.at "abcdef" 2) "c")) +(check-sat) diff --git a/regression/smt2_strings/str_at_const_unsat/str_at_const_unsat.desc b/regression/smt2_strings/str_at_const_unsat/str_at_const_unsat.desc new file mode 100644 index 00000000000..c58740ea9d7 --- /dev/null +++ b/regression/smt2_strings/str_at_const_unsat/str_at_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +str_at_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/str_at_const_unsat/str_at_const_unsat.smt2 b/regression/smt2_strings/str_at_const_unsat/str_at_const_unsat.smt2 new file mode 100644 index 00000000000..be84f684624 --- /dev/null +++ b/regression/smt2_strings/str_at_const_unsat/str_at_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (= (str.at "abcdef" 2) "d")) +(check-sat) diff --git a/regression/smt2_strings/str_in_re_const_sat/str_in_re_const_sat.desc b/regression/smt2_strings/str_in_re_const_sat/str_in_re_const_sat.desc new file mode 100644 index 00000000000..0d3b0d956cb --- /dev/null +++ b/regression/smt2_strings/str_in_re_const_sat/str_in_re_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +str_in_re_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/str_in_re_const_sat/str_in_re_const_sat.smt2 b/regression/smt2_strings/str_in_re_const_sat/str_in_re_const_sat.smt2 new file mode 100644 index 00000000000..054efadec78 --- /dev/null +++ b/regression/smt2_strings/str_in_re_const_sat/str_in_re_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "abcdef" (re.* (re.range "a" "f")))) +(check-sat) diff --git a/regression/smt2_strings/str_in_re_const_unsat/str_in_re_const_unsat.desc b/regression/smt2_strings/str_in_re_const_unsat/str_in_re_const_unsat.desc new file mode 100644 index 00000000000..f2200d825e3 --- /dev/null +++ b/regression/smt2_strings/str_in_re_const_unsat/str_in_re_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +str_in_re_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/str_in_re_const_unsat/str_in_re_const_unsat.smt2 b/regression/smt2_strings/str_in_re_const_unsat/str_in_re_const_unsat.smt2 new file mode 100644 index 00000000000..b12b106fa24 --- /dev/null +++ b/regression/smt2_strings/str_in_re_const_unsat/str_in_re_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "abcdef" (re.* (re.range "a" "e")))) +(check-sat) diff --git a/regression/smt2_strings/str_to_int_const_sat/str_to_int_const_sat.desc b/regression/smt2_strings/str_to_int_const_sat/str_to_int_const_sat.desc new file mode 100644 index 00000000000..95cf28b6dbe --- /dev/null +++ b/regression/smt2_strings/str_to_int_const_sat/str_to_int_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +str_to_int_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/str_to_int_const_sat/str_to_int_const_sat.smt2 b/regression/smt2_strings/str_to_int_const_sat/str_to_int_const_sat.smt2 new file mode 100644 index 00000000000..97e5e7c74db --- /dev/null +++ b/regression/smt2_strings/str_to_int_const_sat/str_to_int_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (= (str.to.int "123" ) 123)) +(check-sat) diff --git a/regression/smt2_strings/str_to_int_const_unsat/str_to_int_const_unsat.desc b/regression/smt2_strings/str_to_int_const_unsat/str_to_int_const_unsat.desc new file mode 100644 index 00000000000..98bff2c7006 --- /dev/null +++ b/regression/smt2_strings/str_to_int_const_unsat/str_to_int_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +str_to_int_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/str_to_int_const_unsat/str_to_int_const_unsat.smt2 b/regression/smt2_strings/str_to_int_const_unsat/str_to_int_const_unsat.smt2 new file mode 100644 index 00000000000..b10f33c996b --- /dev/null +++ b/regression/smt2_strings/str_to_int_const_unsat/str_to_int_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (= (str.to.int "123" ) 12)) +(check-sat) diff --git a/regression/smt2_strings/str_to_re_const_sat/str_to_re_const_sat.desc b/regression/smt2_strings/str_to_re_const_sat/str_to_re_const_sat.desc new file mode 100644 index 00000000000..ca29770ae25 --- /dev/null +++ b/regression/smt2_strings/str_to_re_const_sat/str_to_re_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +str_to_re_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/str_to_re_const_sat/str_to_re_const_sat.smt2 b/regression/smt2_strings/str_to_re_const_sat/str_to_re_const_sat.smt2 new file mode 100644 index 00000000000..85819c001e0 --- /dev/null +++ b/regression/smt2_strings/str_to_re_const_sat/str_to_re_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "abba" (re.* (re.union (str.to.re "a") (str.to.re "b"))))) +(check-sat) diff --git a/regression/smt2_strings/str_to_re_const_unsat/str_to_re_const_unsat.desc b/regression/smt2_strings/str_to_re_const_unsat/str_to_re_const_unsat.desc new file mode 100644 index 00000000000..d8cdc40008f --- /dev/null +++ b/regression/smt2_strings/str_to_re_const_unsat/str_to_re_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +str_to_re_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/str_to_re_const_unsat/str_to_re_const_unsat.smt2 b/regression/smt2_strings/str_to_re_const_unsat/str_to_re_const_unsat.smt2 new file mode 100644 index 00000000000..9ae613885ed --- /dev/null +++ b/regression/smt2_strings/str_to_re_const_unsat/str_to_re_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (str.in.re "abba" (re.* (re.union (str.to.re "a") (str.to.re "c"))))) +(check-sat) diff --git a/regression/smt2_strings/substr_const_sat/substr_const_sat.desc b/regression/smt2_strings/substr_const_sat/substr_const_sat.desc new file mode 100644 index 00000000000..d9dcea44083 --- /dev/null +++ b/regression/smt2_strings/substr_const_sat/substr_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +substr_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/substr_const_sat/substr_const_sat.smt2 b/regression/smt2_strings/substr_const_sat/substr_const_sat.smt2 new file mode 100644 index 00000000000..05267d28e7d --- /dev/null +++ b/regression/smt2_strings/substr_const_sat/substr_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (= (str.substr "abcdef" 2 3) "cde")) +(check-sat) diff --git a/regression/smt2_strings/substr_const_unsat/substr_const_unsat.desc b/regression/smt2_strings/substr_const_unsat/substr_const_unsat.desc new file mode 100644 index 00000000000..b4e3af8bb57 --- /dev/null +++ b/regression/smt2_strings/substr_const_unsat/substr_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +substr_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/substr_const_unsat/substr_const_unsat.smt2 b/regression/smt2_strings/substr_const_unsat/substr_const_unsat.smt2 new file mode 100644 index 00000000000..d17a91435f5 --- /dev/null +++ b/regression/smt2_strings/substr_const_unsat/substr_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (= (str.substr "abcdef" 2 3) "cd")) +(check-sat) diff --git a/regression/smt2_strings/suffixof_const_sat/suffixof_const_sat.desc b/regression/smt2_strings/suffixof_const_sat/suffixof_const_sat.desc new file mode 100644 index 00000000000..0efe7da4991 --- /dev/null +++ b/regression/smt2_strings/suffixof_const_sat/suffixof_const_sat.desc @@ -0,0 +1,8 @@ +FUTURE +suffixof_const_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error diff --git a/regression/smt2_strings/suffixof_const_sat/suffixof_const_sat.smt2 b/regression/smt2_strings/suffixof_const_sat/suffixof_const_sat.smt2 new file mode 100644 index 00000000000..46cd3167f22 --- /dev/null +++ b/regression/smt2_strings/suffixof_const_sat/suffixof_const_sat.smt2 @@ -0,0 +1,2 @@ +(assert (str.suffixof "def" "abcdef")) +(check-sat) diff --git a/regression/smt2_strings/suffixof_const_unsat/suffixof_const_unsat.desc b/regression/smt2_strings/suffixof_const_unsat/suffixof_const_unsat.desc new file mode 100644 index 00000000000..b3fac36f8c9 --- /dev/null +++ b/regression/smt2_strings/suffixof_const_unsat/suffixof_const_unsat.desc @@ -0,0 +1,8 @@ +FUTURE +suffixof_const_unsat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +error diff --git a/regression/smt2_strings/suffixof_const_unsat/suffixof_const_unsat.smt2 b/regression/smt2_strings/suffixof_const_unsat/suffixof_const_unsat.smt2 new file mode 100644 index 00000000000..4195c2beb74 --- /dev/null +++ b/regression/smt2_strings/suffixof_const_unsat/suffixof_const_unsat.smt2 @@ -0,0 +1,2 @@ +(assert (str.suffixof "de" "abcdef")) +(check-sat)