From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Sun, 10 Jun 2018 02:13:28 +0000 (-0700)
Subject: Disable test that fails in competition mode (#2063)
X-Git-Tag: cvc5-1.0.0~4970
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f64824685c9342466249e1eabca53b5c04c0aed2;p=cvc5.git

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 8f76c798a..986527f98 100644
--- 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;