summaryrefslogtreecommitdiff
path: root/test/regress/regress1/error.cvc
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2018-06-14 09:57:30 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2018-06-14 09:57:30 -0500
commit9529702399dca846212547b8165464c0f1fce154 (patch)
tree1a55d3f4c8e5a9047f645b8c366b6fdc9cfba598 /test/regress/regress1/error.cvc
parenta255983362f043fb1831e5f53ed11c787d9b224f (diff)
parentea24eec6b7914550c84cb09c569b7fc80304d8e7 (diff)
Merge branch 'master' of https://github.com/CVC4/CVC4 into sygusComp2018-2
Diffstat (limited to 'test/regress/regress1/error.cvc')
-rw-r--r--test/regress/regress1/error.cvc3
1 files changed, 2 insertions, 1 deletions
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback