summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2019-10-14 14:21:32 -0700
committerGitHub <noreply@github.com>2019-10-14 14:21:32 -0700
commit8c451415de55e27b24a204a0d35c07722bc832fc (patch)
treeb053eb3565b9a6256570ece65c381de14e81ebaf
parent366a361ad46e81972f5631fd5df8f725d0e2f4bc (diff)
Disable regression test for competition build (#3388)
This commit disables a regression test that was failing for the competition build due to not emitting the expected error message.
-rw-r--r--test/regress/regress0/sygus/no-logic.sy9
1 files changed, 5 insertions, 4 deletions
diff --git a/test/regress/regress0/sygus/no-logic.sy b/test/regress/regress0/sygus/no-logic.sy
index 76584d265..06fc876cd 100644
--- a/test/regress/regress0/sygus/no-logic.sy
+++ b/test/regress/regress0/sygus/no-logic.sy
@@ -1,8 +1,9 @@
+; REQUIRE: no-competition
; COMMAND-LINE: --sygus-out=status --lang=sygus2
-; EXPECT-ERROR: no-logic.sy:7.10: No set-logic command was given before this point.
-; EXPECT-ERROR: no-logic.sy:7.10: CVC4 will make all theories available.
-; EXPECT-ERROR: no-logic.sy:7.10: Consider setting a stricter logic for (likely) better performance.
-; EXPECT-ERROR: no-logic.sy:7.10: To suppress this warning in the future use (set-logic ALL).
+; EXPECT-ERROR: no-logic.sy:8.10: No set-logic command was given before this point.
+; EXPECT-ERROR: no-logic.sy:8.10: CVC4 will make all theories available.
+; EXPECT-ERROR: no-logic.sy:8.10: Consider setting a stricter logic for (likely) better performance.
+; EXPECT-ERROR: no-logic.sy:8.10: To suppress this warning in the future use (set-logic ALL).
; EXPECT: unsat
(synth-fun f ((x Int)) Int
((Start Int))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback