diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2018-06-14 09:57:30 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2018-06-14 09:57:30 -0500 |
commit | 9529702399dca846212547b8165464c0f1fce154 (patch) | |
tree | 1a55d3f4c8e5a9047f645b8c366b6fdc9cfba598 /test/regress/regress1/error.cvc | |
parent | a255983362f043fb1831e5f53ed11c787d9b224f (diff) | |
parent | ea24eec6b7914550c84cb09c569b7fc80304d8e7 (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.cvc | 3 |
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; |