From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 16 Jun 2020 17:57:08 +0000 (-0700)
Subject: Add missing REQUIRES to new regressions. (#4625)
X-Git-Tag: cvc5-1.0.0~3210
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ab004e470f5094145c71a2591fdeec658cd9eb2f;p=cvc5.git

Add missing REQUIRES to new regressions. (#4625)
---

diff --git a/test/regress/regress0/bv/issue-4075.smt2 b/test/regress/regress0/bv/issue-4075.smt2
index ea1be9421..083fbf897 100644
--- a/test/regress/regress0/bv/issue-4075.smt2
+++ b/test/regress/regress0/bv/issue-4075.smt2
@@ -1,4 +1,5 @@
-; EXPECT: (error "Parse Error: issue-4075.smt2:10.26: expecting number of repeats > 0
+; REQUIRES: no-competition
+; EXPECT: (error "Parse Error: issue-4075.smt2:11.26: expecting number of repeats > 0
 ; EXPECT:
 ; EXPECT:  (simplify ((_ repeat 0) b))
 ; EXPECT:                       ^
diff --git a/test/regress/regress0/bv/issue-4076.smt2 b/test/regress/regress0/bv/issue-4076.smt2
index 3a80dc5f0..c52d2169a 100644
--- a/test/regress/regress0/bv/issue-4076.smt2
+++ b/test/regress/regress0/bv/issue-4076.smt2
@@ -2,7 +2,6 @@
 ; EXPECT: sat
 ; EXPECT: sat
 (set-logic ALL)
-(set-option :produce-models true)
 (declare-fun a ((_ BitVec 2)) Int)
 (declare-fun b (Int) (_ BitVec 2))
 (declare-const c Int)
diff --git a/test/regress/regress0/bv/issue-4130.smt2 b/test/regress/regress0/bv/issue-4130.smt2
index aa4a13068..4c7daab57 100644
--- a/test/regress/regress0/bv/issue-4130.smt2
+++ b/test/regress/regress0/bv/issue-4130.smt2
@@ -1,4 +1,5 @@
-; EXPECT: (error "Parse Error: issue-4130.smt2:9.39: expecting bit-width > 0
+; REQUIRES: no-competition
+; EXPECT: (error "Parse Error: issue-4130.smt2:10.39: expecting bit-width > 0
 ; EXPECT:
 ; EXPECT:   (assert (and (= a (bv2nat ((_ int2bv 0) a)))))
 ; EXPECT:                                        ^