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 ea1be9421da724f9870fb23cd078b6d90ff13071..083fbf897ee26b0463a59fcad5a096b465630c51 100644 (file)
--- 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 3a80dc5f01f7469872c6ce045d690f03f236373c..c52d2169a55cb9fe1d0abdbc1ab2be395167864a 100644 (file)
--- 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 aa4a13068e5c27cc8571a03e13dc8815c1e3bcd1..4c7daab5756cef9095a77ea9d49aa7d72088b25e 100644 (file)
--- 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:                                        ^