diff --git a/regression/smt2_strings/README.md b/regression/smt2_strings/README.md index 18afac444f3..dcc0bf22f25 100644 --- a/regression/smt2_strings/README.md +++ b/regression/smt2_strings/README.md @@ -1,14 +1,32 @@ Test Suite for SMT2 String Operations ===================================== -The purpose of this suite is to test the level of string support of cbmc's smt2 +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 +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 +../test.pl -p -CKFT -c ``` -(note the `-F` option to consider all tests tagged as "FUTURE"). +(note the `-CKFT` option to consider all testing levels ("CORE", "KNOWNBUG", +"FUTURE", "THOROUGH"), as these are relevant to CBMC only. +More specifically, tests are tagged according to the expected support by the +3rd party solver. The commands below will only run the tests where support is +expected: + +CVC4: +``` +../test.pl -p -CKFT -X cvc4_bug -c +``` +Note: Most of the string operations are only supported when cvc4 is passed the +`--strings-exp` option. For running the tests, suggest creating a script that +calls cvc4 with `--strings-exp`, and pass the path to that script to the +command above. + +Z3: +``` +../test.pl -p -CKFT -X z3_bug -c +``` diff --git a/regression/smt2_strings/indexof_input_sat/indexof_input_sat.desc b/regression/smt2_strings/indexof_input_sat/indexof_input_sat.desc index feb66395696..26b96300a3b 100644 --- a/regression/smt2_strings/indexof_input_sat/indexof_input_sat.desc +++ b/regression/smt2_strings/indexof_input_sat/indexof_input_sat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug indexof_input_sat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ indexof_input_sat.smt2 ^sat$ -- error +-- +z3: +Returns "unknown" +Z3 [version 4.8.3 - 64 bit] 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 index 292fa9cf69b..1359e02f819 100644 --- 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 @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug lex_order_const_sat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ lex_order_const_sat.smt2 ^sat$ -- error +-- +z3: +str.< not supported +Z3 [version 4.8.3 - 64 bit] 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 index 2d26a665b6f..d6158a3213c 100644 --- 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 @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug lex_order_const_unsat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ lex_order_const_unsat.smt2 ^unsat$ -- error +-- +z3: +str.< not supported +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/lex_order_input_sat/lex_order_input_sat.desc b/regression/smt2_strings/lex_order_input_sat/lex_order_input_sat.desc index 1f3c1590492..4279be4f455 100644 --- a/regression/smt2_strings/lex_order_input_sat/lex_order_input_sat.desc +++ b/regression/smt2_strings/lex_order_input_sat/lex_order_input_sat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug lex_order_input_sat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ lex_order_input_sat.smt2 ^sat$ -- error +-- +z3: +str.< not supported +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/lex_order_input_unsat/lex_order_input_unsat.desc b/regression/smt2_strings/lex_order_input_unsat/lex_order_input_unsat.desc index de9a042eab4..384a342d7c3 100644 --- a/regression/smt2_strings/lex_order_input_unsat/lex_order_input_unsat.desc +++ b/regression/smt2_strings/lex_order_input_unsat/lex_order_input_unsat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug lex_order_input_unsat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ lex_order_input_unsat.smt2 ^unsat$ -- error +-- +z3: +str.< not supported +Z3 [version 4.8.3 - 64 bit] 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 index e8edec2152e..ef3fb19bd37 100644 --- 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 @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug reflexive_lex_order_const_sat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ reflexive_lex_order_const_sat.smt2 ^sat$ -- error +-- +z3: +str.<= not supported +Z3 [version 4.8.3 - 64 bit] 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 index 841b14c51cf..1c2b4399185 100644 --- 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 @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug reflexive_lex_order_const_sat2.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ reflexive_lex_order_const_sat2.smt2 ^sat$ -- error +-- +z3: +str.<= not supported +Z3 [version 4.8.3 - 64 bit] 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 index d529e827013..75d87268c52 100644 --- 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 @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug reflexive_lex_order_const_unsat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ reflexive_lex_order_const_unsat.smt2 ^unsat$ -- error +-- +z3: +str.<= not supported +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/reflexive_lex_order_input_sat/reflexive_lex_order_input_sat.desc b/regression/smt2_strings/reflexive_lex_order_input_sat/reflexive_lex_order_input_sat.desc index de3c8a2903f..9e5718cb598 100644 --- a/regression/smt2_strings/reflexive_lex_order_input_sat/reflexive_lex_order_input_sat.desc +++ b/regression/smt2_strings/reflexive_lex_order_input_sat/reflexive_lex_order_input_sat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug reflexive_lex_order_input_sat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ reflexive_lex_order_input_sat.smt2 ^sat$ -- error +-- +z3: +str.<= not supported +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/reflexive_lex_order_input_unsat/reflexive_lex_order_input_unsat.desc b/regression/smt2_strings/reflexive_lex_order_input_unsat/reflexive_lex_order_input_unsat.desc index 8fbebbd2412..a8cbae0421f 100644 --- a/regression/smt2_strings/reflexive_lex_order_input_unsat/reflexive_lex_order_input_unsat.desc +++ b/regression/smt2_strings/reflexive_lex_order_input_unsat/reflexive_lex_order_input_unsat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug reflexive_lex_order_input_unsat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ reflexive_lex_order_input_unsat.smt2 ^unsat$ -- error +-- +z3: +str.<= not supported +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/regexp_all_sat/regexp_all_sat.desc b/regression/smt2_strings/regexp_all_sat/regexp_all_sat.desc index 20043a5d587..34bb3f01063 100644 --- a/regression/smt2_strings/regexp_all_sat/regexp_all_sat.desc +++ b/regression/smt2_strings/regexp_all_sat/regexp_all_sat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE cvc4_bug regexp_all_sat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ regexp_all_sat.smt2 ^sat$ -- error +-- +cvc4 (--strings-exp): +re.all not supported +(cvc4 1.7-prerelease [git master e1dc3932]) diff --git a/regression/smt2_strings/regexp_concat_input_sat/regexp_concat_input_sat.desc b/regression/smt2_strings/regexp_concat_input_sat/regexp_concat_input_sat.desc index 3b6fb76aa67..93f99fc1f2a 100644 --- a/regression/smt2_strings/regexp_concat_input_sat/regexp_concat_input_sat.desc +++ b/regression/smt2_strings/regexp_concat_input_sat/regexp_concat_input_sat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug regexp_concat_input_sat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ regexp_concat_input_sat.smt2 ^sat$ -- error +-- +z3: +Returns "unknown" +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/regexp_concat_input_unsat/regexp_concat_input_unsat.desc b/regression/smt2_strings/regexp_concat_input_unsat/regexp_concat_input_unsat.desc index e5e91e04be0..16b01858460 100644 --- a/regression/smt2_strings/regexp_concat_input_unsat/regexp_concat_input_unsat.desc +++ b/regression/smt2_strings/regexp_concat_input_unsat/regexp_concat_input_unsat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE cvc4_bug z3_bug regexp_concat_input_unsat.smt2 ^EXIT=0$ @@ -6,3 +6,13 @@ regexp_concat_input_unsat.smt2 ^unsat$ -- error +-- +cvc4 (--strings-exp): +Erroneously returns SAT. +The obtained model is rubbish too, it assumes that +"abc" matches "A"* + "ab"* +(cvc4 1.7-prerelease [git master e1dc3932]) + +z3: +Returns "unknown" +Z3 [version 4.8.3 - 64 bit] 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 index 0a761e22d58..9c1a1110a4a 100644 --- 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 @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug regexp_inter_const_unsat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ regexp_inter_const_unsat.smt2 ^unsat$ -- error +-- +z3: +Erroneously returns "sat" +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/regexp_inter_input_sat/regexp_inter_input_sat.desc b/regression/smt2_strings/regexp_inter_input_sat/regexp_inter_input_sat.desc index 8640d88d10f..7817d738093 100644 --- a/regression/smt2_strings/regexp_inter_input_sat/regexp_inter_input_sat.desc +++ b/regression/smt2_strings/regexp_inter_input_sat/regexp_inter_input_sat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug regexp_inter_input_sat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ regexp_inter_input_sat.smt2 ^sat$ -- error +-- +z3: +Returns "unknown" +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/regexp_inter_input_unsat/regexp_inter_input_unsat.desc b/regression/smt2_strings/regexp_inter_input_unsat/regexp_inter_input_unsat.desc index 2a31b103734..7679f5a2eba 100644 --- a/regression/smt2_strings/regexp_inter_input_unsat/regexp_inter_input_unsat.desc +++ b/regression/smt2_strings/regexp_inter_input_unsat/regexp_inter_input_unsat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE cvc4_bug z3_bug regexp_inter_input_unsat.smt2 ^EXIT=0$ @@ -6,3 +6,13 @@ regexp_inter_input_unsat.smt2 ^unsat$ -- error +-- +cvc4 (--strings-exp): +re.inter seems to not be constrained enough, as +(assert (str.in.re "abc" (re.inter (str.to.re in1) (str.to.re in2)))) +allows a model where in1=="abc" and in2=="a". +(cvc4 1.7-prerelease [git master e1dc3932]) + +z3: +Returns "unknown" +Z3 [version 4.8.3 - 64 bit] 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 index 1f392b09c5f..24a322fe85b 100644 --- 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 @@ -1,4 +1,4 @@ -FUTURE +FUTURE cvc4_bug regexp_loop_const_sat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ regexp_loop_const_sat.smt2 ^sat$ -- error +-- +cvc4 (--strings-exp): +re.loop not supported +(cvc4 1.7-prerelease [git master e1dc3932]) 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 index c542ca386dc..b907002640d 100644 --- 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 @@ -1,4 +1,4 @@ -FUTURE +FUTURE cvc4_bug regexp_loop_const_unsat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ regexp_loop_const_unsat.smt2 ^unsat$ -- error +-- +cvc4 (--strings-exp): +re.loop not supported +(cvc4 1.7-prerelease [git master e1dc3932]) diff --git a/regression/smt2_strings/regexp_loop_input_sat/regexp_loop_input_sat.desc b/regression/smt2_strings/regexp_loop_input_sat/regexp_loop_input_sat.desc index 1324519eabc..c0948bde7d5 100644 --- a/regression/smt2_strings/regexp_loop_input_sat/regexp_loop_input_sat.desc +++ b/regression/smt2_strings/regexp_loop_input_sat/regexp_loop_input_sat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE cvc4_bug z3_bug regexp_loop_input_sat.smt2 ^EXIT=0$ @@ -6,3 +6,11 @@ regexp_loop_input_sat.smt2 ^sat$ -- error +-- +cvc4 (--strings-exp): +re.loop not supported +(cvc4 1.7-prerelease [git master e1dc3932]) + +z3: +re.loop is only supported with constant bounds +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/regexp_loop_input_unsat/regexp_loop_input_unsat.desc b/regression/smt2_strings/regexp_loop_input_unsat/regexp_loop_input_unsat.desc index b2008f4cdc9..c5046449c8d 100644 --- a/regression/smt2_strings/regexp_loop_input_unsat/regexp_loop_input_unsat.desc +++ b/regression/smt2_strings/regexp_loop_input_unsat/regexp_loop_input_unsat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE cvc4_bug z3_bug regexp_loop_input_unsat.smt2 ^EXIT=0$ @@ -6,3 +6,11 @@ regexp_loop_input_unsat.smt2 ^unsat$ -- error +-- +cvc4 (--strings-exp): +re.loop not supported +(cvc4 1.7-prerelease [git master e1dc3932]) + +z3: +re.loop is only supported with constant bounds +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/regexp_opt_input_sat/regexp_opt_input_sat.desc b/regression/smt2_strings/regexp_opt_input_sat/regexp_opt_input_sat.desc index 55503f02cd5..3841b017e14 100644 --- a/regression/smt2_strings/regexp_opt_input_sat/regexp_opt_input_sat.desc +++ b/regression/smt2_strings/regexp_opt_input_sat/regexp_opt_input_sat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug regexp_opt_input_sat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ regexp_opt_input_sat.smt2 ^sat$ -- error + +z3: +Returns "unknown" +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/regexp_plus_input_sat/regexp_plus_input_sat.desc b/regression/smt2_strings/regexp_plus_input_sat/regexp_plus_input_sat.desc index bd701b3624a..4614faa7a03 100644 --- a/regression/smt2_strings/regexp_plus_input_sat/regexp_plus_input_sat.desc +++ b/regression/smt2_strings/regexp_plus_input_sat/regexp_plus_input_sat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug regexp_plus_input_sat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ regexp_plus_input_sat.smt2 ^sat$ -- error +-- +z3: +Returns "unknown" +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/regexp_plus_input_unsat/regexp_plus_input_unsat.desc b/regression/smt2_strings/regexp_plus_input_unsat/regexp_plus_input_unsat.desc index 61998198208..3968bc68a6f 100644 --- a/regression/smt2_strings/regexp_plus_input_unsat/regexp_plus_input_unsat.desc +++ b/regression/smt2_strings/regexp_plus_input_unsat/regexp_plus_input_unsat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug regexp_plus_input_unsat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ regexp_plus_input_unsat.smt2 ^unsat$ -- error +-- +z3: +Returns "unknown" +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/regexp_range_input_sat/regexp_range_input_sat.desc b/regression/smt2_strings/regexp_range_input_sat/regexp_range_input_sat.desc index 3ae65245345..6ec40b797d5 100644 --- a/regression/smt2_strings/regexp_range_input_sat/regexp_range_input_sat.desc +++ b/regression/smt2_strings/regexp_range_input_sat/regexp_range_input_sat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE cvc4_bug z3_bug regexp_range_input_sat.smt2 ^EXIT=0$ @@ -6,3 +6,11 @@ regexp_range_input_sat.smt2 ^sat$ -- error +-- +cvc4 (--strings-exp): +re.range expects constant bounds +(cvc4 1.7-prerelease [git master e1dc3932]) + +z3: +Returns "unknown" +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/regexp_range_input_unsat/regexp_range_input_unsat.desc b/regression/smt2_strings/regexp_range_input_unsat/regexp_range_input_unsat.desc index 7e2434cddc0..5508d7ac8a9 100644 --- a/regression/smt2_strings/regexp_range_input_unsat/regexp_range_input_unsat.desc +++ b/regression/smt2_strings/regexp_range_input_unsat/regexp_range_input_unsat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE cvc4_bug z3_bug regexp_range_input_unsat.smt2 ^EXIT=0$ @@ -6,3 +6,11 @@ regexp_range_input_unsat.smt2 ^unsat$ -- error +-- +cvc4 (--strings-exp): +re.range expects constant bounds +(cvc4 1.7-prerelease [git master e1dc3932]) + +z3: +Returns "unknown" +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/regexp_star_input_sat/regexp_star_input_sat.desc b/regression/smt2_strings/regexp_star_input_sat/regexp_star_input_sat.desc index 6a64f30fa1f..c7474e8f139 100644 --- a/regression/smt2_strings/regexp_star_input_sat/regexp_star_input_sat.desc +++ b/regression/smt2_strings/regexp_star_input_sat/regexp_star_input_sat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug regexp_star_input_sat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ regexp_star_input_sat.smt2 ^sat$ -- error +-- +z3: +Returns "unknown" +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/regexp_union_input_sat/regexp_union_const_sat.desc b/regression/smt2_strings/regexp_union_input_sat/regexp_union_const_sat.desc deleted file mode 100644 index 8da32c9b14e..00000000000 --- a/regression/smt2_strings/regexp_union_input_sat/regexp_union_const_sat.desc +++ /dev/null @@ -1,8 +0,0 @@ -FUTURE -regexp_union_const_sat.smt2 - -^EXIT=0$ -^SIGNAL=0$ -^sat$ --- -error diff --git a/regression/smt2_strings/regexp_union_input_sat/regexp_union_input_sat.desc b/regression/smt2_strings/regexp_union_input_sat/regexp_union_input_sat.desc new file mode 100644 index 00000000000..cf1f3ea11d9 --- /dev/null +++ b/regression/smt2_strings/regexp_union_input_sat/regexp_union_input_sat.desc @@ -0,0 +1,12 @@ +FUTURE z3_bug +regexp_union_input_sat.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^sat$ +-- +error +-- +z3: +Returns "unknown" +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/regexp_union_input_sat/regexp_union_const_sat.smt2 b/regression/smt2_strings/regexp_union_input_sat/regexp_union_input_sat.smt2 similarity index 100% rename from regression/smt2_strings/regexp_union_input_sat/regexp_union_const_sat.smt2 rename to regression/smt2_strings/regexp_union_input_sat/regexp_union_input_sat.smt2 diff --git a/regression/smt2_strings/regexp_union_input_unsat/regexp_union_const_unsat.desc b/regression/smt2_strings/regexp_union_input_unsat/regexp_union_const_unsat.desc index 8b5e27dafe8..50a511787f8 100644 --- a/regression/smt2_strings/regexp_union_input_unsat/regexp_union_const_unsat.desc +++ b/regression/smt2_strings/regexp_union_input_unsat/regexp_union_const_unsat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug regexp_union_const_unsat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ regexp_union_const_unsat.smt2 ^unsat$ -- error +-- +z3: +Returns "unknown" +Z3 [version 4.8.3 - 64 bit] 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 index dbb6ba8d48a..12ea87d5e1b 100644 --- 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 @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug replace_all_const_sat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ replace_all_const_sat.smt2 ^sat$ -- error +-- +z3: +str.replaceall is not supported +Z3 [version 4.8.3 - 64 bit] 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 index 7f6bfff8b9b..92d1a0113f8 100644 --- 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 @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug replace_all_const_unsat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ replace_all_const_unsat.smt2 ^unsat$ -- error +-- +z3: +str.replaceall is not supported +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/replace_all_input_sat/replace_all_const_sat.desc b/regression/smt2_strings/replace_all_input_sat/replace_all_const_sat.desc index dbb6ba8d48a..12ea87d5e1b 100644 --- a/regression/smt2_strings/replace_all_input_sat/replace_all_const_sat.desc +++ b/regression/smt2_strings/replace_all_input_sat/replace_all_const_sat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug replace_all_const_sat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ replace_all_const_sat.smt2 ^sat$ -- error +-- +z3: +str.replaceall is not supported +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/replace_input_sat/replace_input_sat.desc b/regression/smt2_strings/replace_input_sat/replace_input_sat.desc index a04d67ef2c4..f26eb2d532e 100644 --- a/regression/smt2_strings/replace_input_sat/replace_input_sat.desc +++ b/regression/smt2_strings/replace_input_sat/replace_input_sat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug replace_input_sat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ replace_input_sat.smt2 ^sat$ -- error +-- +z3: +Returns "unknown" +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/str_in_re_input_sat/str_in_re_input_sat.desc b/regression/smt2_strings/str_in_re_input_sat/str_in_re_input_sat.desc index e02a3a3f860..6fa3780fd0e 100644 --- a/regression/smt2_strings/str_in_re_input_sat/str_in_re_input_sat.desc +++ b/regression/smt2_strings/str_in_re_input_sat/str_in_re_input_sat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug str_in_re_input_sat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ str_in_re_input_sat.smt2 ^sat$ -- error +-- +z3: +Returns "unknown" +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/str_in_re_input_unsat/str_in_re_input_unsat.desc b/regression/smt2_strings/str_in_re_input_unsat/str_in_re_input_unsat.desc index 4517cb31778..010d439dfb5 100644 --- a/regression/smt2_strings/str_in_re_input_unsat/str_in_re_input_unsat.desc +++ b/regression/smt2_strings/str_in_re_input_unsat/str_in_re_input_unsat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug str_in_re_input_unsat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ str_in_re_input_unsat.smt2 ^unsat$ -- error +-- +z3: +Returns "unknown" +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/str_to_re_input_sat/str_to_re_input_sat.desc b/regression/smt2_strings/str_to_re_input_sat/str_to_re_input_sat.desc index a80ce688a87..c79fdfdc08f 100644 --- a/regression/smt2_strings/str_to_re_input_sat/str_to_re_input_sat.desc +++ b/regression/smt2_strings/str_to_re_input_sat/str_to_re_input_sat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug str_to_re_input_sat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ str_to_re_input_sat.smt2 ^sat$ -- error +-- +z3: +Returns "unknown" +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/str_to_re_input_unsat/str_to_re_input_sat.desc b/regression/smt2_strings/str_to_re_input_unsat/str_to_re_input_sat.desc index d8fff3e390e..340dad713fb 100644 --- a/regression/smt2_strings/str_to_re_input_unsat/str_to_re_input_sat.desc +++ b/regression/smt2_strings/str_to_re_input_unsat/str_to_re_input_sat.desc @@ -1,4 +1,4 @@ -FUTURE +FUTURE z3_bug str_to_re_input_sat.smt2 ^EXIT=0$ @@ -6,3 +6,7 @@ str_to_re_input_sat.smt2 ^unsat$ -- error +-- +z3: +Returns "unknown" +Z3 [version 4.8.3 - 64 bit] diff --git a/regression/smt2_strings/suffixof_input_sat/suffixof_input_sat.smt2 b/regression/smt2_strings/suffixof_input_sat/suffixof_input_sat.smt2 index 4b51336ced3..af71776db63 100644 --- a/regression/smt2_strings/suffixof_input_sat/suffixof_input_sat.smt2 +++ b/regression/smt2_strings/suffixof_input_sat/suffixof_input_sat.smt2 @@ -4,4 +4,3 @@ (assert (not (= str suffix))) (assert (str.suffixof suffix str)) (check-sat) -(get-model)