Skip 3rd party cvc4 known bugs

Skip all tests that are known to fail for cvc4 1.7-prerelease.

Author: Joel Allred

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_unsat/regexp_concat_input_unsat.desc

@@ -1,8 +1,14 @@
-FUTURE
+FUTURE cvc4_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])

regression/smt2_strings/regexp_inter_input_unsat/regexp_inter_input_unsat.desc

@@ -1,8 +1,15 @@
-FUTURE
+FUTURE cvc4_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])
+

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,12 @@
-FUTURE
+FUTURE cvc4_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])

regression/smt2_strings/regexp_loop_input_unsat/regexp_loop_input_unsat.desc

@@ -1,8 +1,12 @@
-FUTURE
+FUTURE cvc4_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])

regression/smt2_strings/regexp_range_input_sat/regexp_range_input_sat.desc

@@ -1,8 +1,12 @@
-FUTURE
+FUTURE cvc4_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])

regression/smt2_strings/regexp_range_input_unsat/regexp_range_input_unsat.desc

@@ -1,8 +1,13 @@
-FUTURE
+FUTURE cvc4_bug
 regexp_range_input_unsat.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^unsat$
 --
 error
+--
+cvc4 (--strings-exp):
+re.range expects constant bounds
+(cvc4 1.7-prerelease [git master e1dc3932])
+