From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 7 Jul 2021 16:08:24 +0000 (-0500)
Subject: Fix regressions for competition build (#6846)
X-Git-Tag: cvc5-1.0.0~1519
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ab2d074e105a1271eee0595f17730eeb7143e933;p=cvc5.git

Fix regressions for competition build (#6846)

Fixes one of the issues in the nightlies.
---

diff --git a/test/regress/regress0/sygus/print-debug.sy b/test/regress/regress0/sygus/print-debug.sy
index 08b2f7c50..18da0feea 100644
--- 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 7b943f479..55338bf6c 100644
--- 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)