Disable test that fails in competition mode (#2063)

Commit 106e764a04e4099cc36d13de9cec47cbf717b6cc missed one test case.
This commit disables that test case for the competition build.

diff --git a/test/regress/regress1/error.cvc b/test/regress/regress1/error.cvc
index 8f76c798a6b088c184af583ebe7c775a2fbdf29c..986527f98695b1b1507f266b364f7001b4303c78 100644 (file)
--- a/test/regress/regress1/error.cvc
+++ b/test/regress/regress1/error.cvc
@@ -1,6 +1,7 @@
+% REQUIRES: no-competition
 % ERROR-SCRUBBER: sed -e '/^[[:space:]]*$/d'
 % EXPECT-ERROR: CVC4 Error:
-% EXPECT-ERROR: Parse Error: error.cvc:6.8: Symbol 'BOOL' not declared as a type
+% EXPECT-ERROR: Parse Error: error.cvc:7.8: Symbol 'BOOL' not declared as a type
 % EXPECT-ERROR:   p : BOOL;
 % EXPECT-ERROR:       ^
 p : BOOL;