summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sygus
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/sygus')
-rw-r--r--test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy3
1 files changed, 2 insertions, 1 deletions
diff --git a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy
index 7a90d7427..1b5690d3a 100644
--- a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy
+++ b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy
@@ -1,6 +1,7 @@
+; REQUIRES: no-competition
; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2
; EXPECT-ERROR: CVC4 Error:
-; EXPECT-ERROR: Parse Error: pLTL-sygus-syntax-err.sy:79.19: number of arguments does not match the constructor type
+; EXPECT-ERROR: Parse Error: pLTL-sygus-syntax-err.sy:80.19: number of arguments does not match the constructor type
; EXPECT-ERROR:
; EXPECT-ERROR: (Op2 <O2> <F>)
; EXPECT-ERROR: ^
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback