Merge pull request diffblue#4453 from allredj/smt2-3rdparty-knownbugs

Add test passing status info for Z3 and CVC4

Author: tautschnig

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 <path_to_solver_binary>
+../test.pl -p -CKFT -c <path_to_solver_binary>
 ```
 
-(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 <path_to_cvc4_binary>
+```
+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 <path_to_z3_binary>
+```

regression/smt2_strings/indexof_input_sat/indexof_input_sat.desc

@@ -1,8 +1,12 @@
-FUTURE
+FUTURE z3_bug
 indexof_input_sat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^sat$
 --
 error
+--
+z3:
+Returns "unknown"
+Z3 [version 4.8.3 - 64 bit]

regression/smt2_strings/lex_order_const_sat/lex_order_const_sat.desc

@@ -1,8 +1,12 @@
-FUTURE
+FUTURE z3_bug
 lex_order_const_sat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^sat$
 --
 error
+--
+z3:
+str.< not supported
+Z3 [version 4.8.3 - 64 bit]

regression/smt2_strings/lex_order_const_unsat/lex_order_const_unsat.desc

@@ -1,8 +1,12 @@
-FUTURE
+FUTURE z3_bug
 lex_order_const_unsat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^unsat$
 --
 error
+--
+z3:
+str.< not supported
+Z3 [version 4.8.3 - 64 bit]

regression/smt2_strings/lex_order_input_sat/lex_order_input_sat.desc

@@ -1,8 +1,12 @@
-FUTURE
+FUTURE z3_bug
 lex_order_input_sat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^sat$
 --
 error
+--
+z3:
+str.< not supported
+Z3 [version 4.8.3 - 64 bit]

regression/smt2_strings/lex_order_input_unsat/lex_order_input_unsat.desc

@@ -1,8 +1,12 @@
-FUTURE
+FUTURE z3_bug
 lex_order_input_unsat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^unsat$
 --
 error
+--
+z3:
+str.< not supported
+Z3 [version 4.8.3 - 64 bit]

regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat.desc

@@ -1,8 +1,12 @@
-FUTURE
+FUTURE z3_bug
 reflexive_lex_order_const_sat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^sat$
 --
 error
+--
+z3:
+str.<= not supported
+Z3 [version 4.8.3 - 64 bit]

regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat2.desc

@@ -1,8 +1,12 @@
-FUTURE
+FUTURE z3_bug
 reflexive_lex_order_const_sat2.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^sat$
 --
 error
+--
+z3:
+str.<= not supported
+Z3 [version 4.8.3 - 64 bit]

regression/smt2_strings/reflexive_lex_order_const_unsat/reflexive_lex_order_const_unsat.desc

@@ -1,8 +1,12 @@
-FUTURE
+FUTURE z3_bug
 reflexive_lex_order_const_unsat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^unsat$
 --
 error
+--
+z3:
+str.<= not supported
+Z3 [version 4.8.3 - 64 bit]

regression/smt2_strings/reflexive_lex_order_input_sat/reflexive_lex_order_input_sat.desc

@@ -1,8 +1,12 @@
-FUTURE
+FUTURE z3_bug
 reflexive_lex_order_input_sat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^sat$
 --
 error
+--
+z3:
+str.<= not supported
+Z3 [version 4.8.3 - 64 bit]

regression/smt2_strings/reflexive_lex_order_input_unsat/reflexive_lex_order_input_unsat.desc

@@ -1,8 +1,12 @@
-FUTURE
+FUTURE z3_bug
 reflexive_lex_order_input_unsat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^unsat$
 --
 error
+--
+z3:
+str.<= not supported
+Z3 [version 4.8.3 - 64 bit]

regression/smt2_strings/regexp_all_sat/regexp_all_sat.desc

@@ -1,8 +1,12 @@
-FUTURE
+FUTURE cvc4_bug
 regexp_all_sat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^sat$
 --
 error
+--
+cvc4 (--strings-exp):
+re.all not supported
+(cvc4 1.7-prerelease [git master e1dc3932])

regression/smt2_strings/regexp_concat_input_sat/regexp_concat_input_sat.desc

@@ -1,8 +1,12 @@
-FUTURE
+FUTURE z3_bug
 regexp_concat_input_sat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^sat$
 --
 error
+--
+z3:
+Returns "unknown"
+Z3 [version 4.8.3 - 64 bit]

regression/smt2_strings/regexp_concat_input_unsat/regexp_concat_input_unsat.desc

@@ -1,8 +1,18 @@
-FUTURE
+FUTURE cvc4_bug z3_bug
 regexp_concat_input_unsat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^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]

regression/smt2_strings/regexp_inter_const_unsat/regexp_inter_const_unsat.desc

@@ -1,8 +1,12 @@
-FUTURE
+FUTURE z3_bug
 regexp_inter_const_unsat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^unsat$
 --
 error
+--
+z3:
+Erroneously returns "sat"
+Z3 [version 4.8.3 - 64 bit]

regression/smt2_strings/regexp_inter_input_sat/regexp_inter_input_sat.desc

@@ -1,8 +1,12 @@
-FUTURE
+FUTURE z3_bug
 regexp_inter_input_sat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^sat$
 --
 error
+--
+z3:
+Returns "unknown"
+Z3 [version 4.8.3 - 64 bit]

regression/smt2_strings/regexp_inter_input_unsat/regexp_inter_input_unsat.desc

@@ -1,8 +1,18 @@
-FUTURE
+FUTURE cvc4_bug z3_bug
 regexp_inter_input_unsat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^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]

regression/smt2_strings/regexp_loop_const_sat/regexp_loop_const_sat.desc

@@ -1,8 +1,12 @@
-FUTURE
+FUTURE cvc4_bug
 regexp_loop_const_sat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^sat$
 --
 error
+--
+cvc4 (--strings-exp):
+re.loop not supported
+(cvc4 1.7-prerelease [git master e1dc3932])

regression/smt2_strings/regexp_loop_const_unsat/regexp_loop_const_unsat.desc

@@ -1,8 +1,12 @@
-FUTURE
+FUTURE cvc4_bug
 regexp_loop_const_unsat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^unsat$
 --
 error
+--
+cvc4 (--strings-exp):
+re.loop not supported
+(cvc4 1.7-prerelease [git master e1dc3932])

regression/smt2_strings/regexp_loop_input_sat/regexp_loop_input_sat.desc

@@ -1,8 +1,16 @@
-FUTURE
+FUTURE cvc4_bug z3_bug
 regexp_loop_input_sat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^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]

regression/smt2_strings/regexp_loop_input_unsat/regexp_loop_input_unsat.desc

@@ -1,8 +1,16 @@
-FUTURE
+FUTURE cvc4_bug z3_bug
 regexp_loop_input_unsat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^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]

regression/smt2_strings/regexp_opt_input_sat/regexp_opt_input_sat.desc

@@ -1,8 +1,12 @@
-FUTURE
+FUTURE z3_bug
 regexp_opt_input_sat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^sat$
 --
 error
+
+z3:
+Returns "unknown"
+Z3 [version 4.8.3 - 64 bit]

regression/smt2_strings/regexp_plus_input_sat/regexp_plus_input_sat.desc

@@ -1,8 +1,12 @@
-FUTURE
+FUTURE z3_bug
 regexp_plus_input_sat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^sat$
 --
 error
+--
+z3:
+Returns "unknown"
+Z3 [version 4.8.3 - 64 bit]

regression/smt2_strings/regexp_plus_input_unsat/regexp_plus_input_unsat.desc

@@ -1,8 +1,12 @@
-FUTURE
+FUTURE z3_bug
 regexp_plus_input_unsat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^unsat$
 --
 error
+--
+z3:
+Returns "unknown"
+Z3 [version 4.8.3 - 64 bit]

regression/smt2_strings/regexp_range_input_sat/regexp_range_input_sat.desc

@@ -1,8 +1,16 @@
-FUTURE
+FUTURE cvc4_bug z3_bug
 regexp_range_input_sat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^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]