diffblue · tautschnig · Feb 1, 2019 · Jan 23, 2019 · Jan 23, 2019 · Jan 31, 2019
diff --git 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
@@ -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/.gitignore b/regression/smt2_strings/.gitignore
@@ -0,0 +1 @@
+!*.smt2
diff --git a/regression/smt2_strings/CMakeLists.txt b/regression/smt2_strings/CMakeLists.txt
@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:smt2_solver>"
+)
diff --git a/regression/smt2_strings/Makefile 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
diff --git a/regression/smt2_strings/README.md 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 <path_to_solver_binary>
+```
+
+(note the `-F` option to consider all tests tagged as "FUTURE").
+
diff --git a/regression/smt2_strings/concat_const_sat/concat_const_sat.desc 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -0,0 +1,2 @@
+(assert (str.in.re "aaab" (re.++ (re.+ (str.to.re "a")) (re.opt (str.to.re "b")))))
+(check-sat)
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		!*.smt2
Copy link Collaborator tautschnig Jan 31, 2019 Choose a reason for hiding this comment The reason will be displayed to describe this comment to others. Learn more. That would mean that Makefile, CMakeLists.txt, .desc are also ignore, which doesn't seem right. Copy link Contributor Author allredj* Jan 31, 2019 Choose a reason for hiding this comment The reason will be displayed to describe this comment to others. Learn more. I don't understand. I need to discard the ignore that is introduced here: https://github.com/diffblue/cbmc/blob/develop/.gitignore#L59 and which is useful on the regression tests where cbmc is run with the `--smt2` option. Copy link Collaborator tautschnig Jan 31, 2019 Choose a reason for hiding this comment The reason will be displayed to describe this comment to others. Learn more. Oops, I wasn't aware of that interaction. Copy link Member kroening Jan 31, 2019 Choose a reason for hiding this comment The reason will be displayed to describe this comment to others. Learn more. I don't think that cbmc still writes the file on disk when run with --smt2? Copy link Contributor Author allredj Jan 31, 2019 Choose a reason for hiding this comment The reason will be displayed to describe this comment to others. Learn more. @kroening some of the regression tests use `--outfile`, e.g. https://github.com/diffblue/cbmc/blob/develop/regression/cbmc/Malloc22/test.desc#L3
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		(assert (= (str.++ "abc" "def" "" "gh") "abcdefgh"))
		(check-sat)
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		(assert (= (str.++ "abc" "cdef") "abcde"))
		(check-sat)
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		(assert (str.contains "abcdef" "bcd"))
		(check-sat)
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		(assert (str.contains "abcdef" "dc"))
		(check-sat)
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		(assert (= (str.indexof "abcdef" "cde" 1) 2))
		(check-sat)
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		(assert (= (int.to.str 1234567890) "1234567890"))
		(check-sat)
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		(assert (str.prefixof "abc" "abcdef"))
		(check-sat)
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		(assert (str.prefixof "bc" "abcdef"))
		(check-sat)
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		(assert (str.in.re "abc" (re.* re.all)))
		(check-sat)