projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 8c45141)
Fix regression (#3393)
authorAndres Noetzli <andres.noetzli@gmail.com>
Tue, 15 Oct 2019 13:08:48 +0000 (06:08 -0700)
committerGitHub <noreply@github.com>
Tue, 15 Oct 2019 13:08:48 +0000 (06:08 -0700)
PR #3388 didn't disable the regression correctly (due to using `REQUIRE`
instead of `REQUIRES`). This commit fixes the issue.

test/regress/regress0/sygus/no-logic.sy patch | blob | history

diff --git a/test/regress/regress0/sygus/no-logic.sy b/test/regress/regress0/sygus/no-logic.sy
index 06fc876cd33103ae38bc9069c62dfb28ec6d28ae..8c97949868e60b7e89a106da3d2cef5da31877e9 100644 (file)
--- a/test/regress/regress0/sygus/no-logic.sy
+++ b/test/regress/regress0/sygus/no-logic.sy
@@ -1,4 +1,4 @@
-; REQUIRE: no-competition
+; REQUIRES: no-competition
 ; COMMAND-LINE: --sygus-out=status --lang=sygus2
 ; 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.