projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: b257f55)
Require statistics for regression (#6714)
authorGereon Kremer <nafur42@gmail.com>
Wed, 9 Jun 2021 14:03:04 +0000 (16:03 +0200)
committerGitHub <noreply@github.com>
Wed, 9 Jun 2021 14:03:04 +0000 (09:03 -0500)
This PR makes a new regression explicitly require statistics.

test/regress/regress0/options/statistics.smt2 patch | blob | history

diff --git a/test/regress/regress0/options/statistics.smt2 b/test/regress/regress0/options/statistics.smt2
index 047c039ee50e1eaaf9434a2af00ba73927726add..ae9d93b6f8cfabd016fe0176cab480fb0c19e7d3 100644 (file)
--- a/test/regress/regress0/options/statistics.smt2
+++ b/test/regress/regress0/options/statistics.smt2
@@ -1,3 +1,4 @@
+; REQUIRES: statistics
 ; EXPECT: false
 ; EXPECT: false
 ; EXPECT: false