projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 4d2cca0)
Disable dumping test for non-dumping builds (#2662)
authorAndres Noetzli <andres.noetzli@gmail.com>
Sat, 20 Oct 2018 14:02:16 +0000 (07:02 -0700)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 20 Oct 2018 14:02:16 +0000 (09:02 -0500)
test/regress/regress0/options/invalid_dump.smt2 patch | blob | history

diff --git a/test/regress/regress0/options/invalid_dump.smt2 b/test/regress/regress0/options/invalid_dump.smt2
index 9f92a7a64d6023aa8adde8d717091c73c1c92ec9..ab6f6db316c1509b4a6163e7e7df634be26c731c 100644 (file)
--- a/test/regress/regress0/options/invalid_dump.smt2
+++ b/test/regress/regress0/options/invalid_dump.smt2
@@ -1,3 +1,4 @@
+; REQUIRES: dumping
 ; COMMAND-LINE: --dump invalidDumpTag
 ; ERROR-SCRUBBER: grep -o "unknown option for --dump"
 ; EXPECT-ERROR: unknown option for --dump