From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 14 Oct 2019 21:21:32 +0000 (-0700)
Subject: Disable regression test for competition build (#3388)
X-Git-Tag: cvc5-1.0.0~3885
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8c451415de55e27b24a204a0d35c07722bc832fc;p=cvc5.git

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.
---

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))