projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: e0824de)
Fix regressions for competition build (#6846)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 7 Jul 2021 16:08:24 +0000 (11:08 -0500)
committerGitHub <noreply@github.com>
Wed, 7 Jul 2021 16:08:24 +0000 (16:08 +0000)
Fixes one of the issues in the nightlies.

test/regress/regress0/sygus/print-debug.sy patch | blob | history
test/regress/regress1/quantifiers/qid-debug-inst.smt2 patch | blob | history

diff --git a/test/regress/regress0/sygus/print-debug.sy b/test/regress/regress0/sygus/print-debug.sy
index 08b2f7c501b3758709ea0cb23466496f053b540c..18da0feea379e074c45144f4b94d045144c18ada 100644 (file)
--- a/test/regress/regress0/sygus/print-debug.sy
+++ b/test/regress/regress0/sygus/print-debug.sy
@@ -1,3 +1,4 @@
+; REQUIRES: no-competition
 ; COMMAND-LINE: -o sygus
 ; EXPECT: (sygus-enum 0)
 ; EXPECT: (sygus-candidate (f 0))
diff --git a/test/regress/regress1/quantifiers/qid-debug-inst.smt2 b/test/regress/regress1/quantifiers/qid-debug-inst.smt2
index 7b943f47931e18dcf165c7f2a8201d5fe06346d0..55338bf6c95e91f5d183e4807d00081130d3fefc 100644 (file)
--- a/test/regress/regress1/quantifiers/qid-debug-inst.smt2
+++ b/test/regress/regress1/quantifiers/qid-debug-inst.smt2
@@ -1,3 +1,4 @@
+; REQUIRES: no-competition
 ; COMMAND-LINE: -o inst --no-check-unsat-cores
 ; EXPECT: (num-instantiations myQuant1 1)
 ; EXPECT: (num-instantiations myQuant2 1)