Skip 3rd party Z3 known bugs

Joel Allred · Joel Allred · commit 9f47f8dd3a42 · 2019-03-28T17:57:16.000Z
diff --git a/regression/smt2_strings/indexof_input_sat/indexof_input_sat.desc b/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]
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
@@ -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]
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
@@ -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]
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
@@ -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]
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
@@ -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]
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
@@ -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]
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
@@ -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]
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
@@ -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]
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
@@ -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]
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
@@ -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]
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
@@ -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]
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
@@ -1,4 +1,4 @@
-FUTURE cvc4_bug
+FUTURE cvc4_bug z3_bug
 regexp_concat_input_unsat.smt2
 
 ^EXIT=0$
@@ -12,3 +12,7 @@ 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
@@ -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]
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
@@ -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]
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
@@ -1,4 +1,4 @@
-FUTURE cvc4_bug
+FUTURE cvc4_bug z3_bug
 regexp_inter_input_unsat.smt2
 
 ^EXIT=0$
@@ -13,3 +13,6 @@ re.inter seems to not be constrained enough, as
 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_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 cvc4_bug
+FUTURE cvc4_bug z3_bug
 regexp_loop_input_sat.smt2
 
 ^EXIT=0$
@@ -10,3 +10,7 @@ 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
@@ -1,4 +1,4 @@
-FUTURE cvc4_bug
+FUTURE cvc4_bug z3_bug
 regexp_loop_input_unsat.smt2
 
 ^EXIT=0$
@@ -10,3 +10,7 @@ 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
@@ -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]
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
@@ -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]
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
@@ -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]
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
@@ -1,4 +1,4 @@
-FUTURE cvc4_bug
+FUTURE cvc4_bug z3_bug
 regexp_range_input_sat.smt2
 
 ^EXIT=0$
@@ -10,3 +10,7 @@ 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
@@ -1,4 +1,4 @@
-FUTURE cvc4_bug
+FUTURE cvc4_bug z3_bug
 regexp_range_input_unsat.smt2
 
 ^EXIT=0$
@@ -11,3 +11,6 @@ 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
@@ -1,8 +1,12 @@
-FUTURE
+FUTURE z3_bug
 regexp_star_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_input_sat.desc b/regression/smt2_strings/regexp_union_input_sat/regexp_union_input_sat.desc
@@ -1,8 +1,12 @@
-FUTURE
+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_unsat/regexp_union_const_unsat.desc b/regression/smt2_strings/regexp_union_input_unsat/regexp_union_const_unsat.desc
@@ -1,8 +1,12 @@
-FUTURE
+FUTURE z3_bug
 regexp_union_const_unsat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^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
@@ -1,8 +1,12 @@
-FUTURE
+FUTURE z3_bug
 replace_all_const_sat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^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
@@ -1,8 +1,12 @@
-FUTURE
+FUTURE z3_bug
 replace_all_const_unsat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^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
@@ -1,8 +1,12 @@
-FUTURE
+FUTURE z3_bug
 replace_all_const_sat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^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
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
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
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
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
