summaryrefslogtreecommitdiff
path: root/test/regress/regress1/error.cvc
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress1/error.cvc')
-rw-r--r--test/regress/regress1/error.cvc7
1 files changed, 7 insertions, 0 deletions
diff --git a/test/regress/regress1/error.cvc b/test/regress/regress1/error.cvc
new file mode 100644
index 000000000..8f76c798a
--- /dev/null
+++ b/test/regress/regress1/error.cvc
@@ -0,0 +1,7 @@
+% 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: p : BOOL;
+% EXPECT-ERROR: ^
+p : BOOL;
+% EXIT: 1
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback