From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri, 7 May 2021 23:23:08 +0000 (-0700)
Subject: Fix and add missing REQUIRE labels for FP regression tests. (#6506)
X-Git-Tag: cvc5-1.0.0~1781
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5bd2fcd60adbfb1f1941d4ed9da6ec10e06dfb12;p=cvc5.git

Fix and add missing REQUIRE labels for FP regression tests. (#6506)
---

diff --git a/test/regress/regress0/fp/from_sbv.smt2 b/test/regress/regress0/fp/from_sbv.smt2
index 226d6589c..3211339d6 100644
--- a/test/regress/regress0/fp/from_sbv.smt2
+++ b/test/regress/regress0/fp/from_sbv.smt2
@@ -1,3 +1,4 @@
+; REQUIRES: symfpu
 ; COMMAND-LINE: --fp-exp
 ; EXPECT: unsat
 (set-logic QF_BVFP)
diff --git a/test/regress/regress0/fp/from_ubv.smt2 b/test/regress/regress0/fp/from_ubv.smt2
index 6939e478a..c02f8d304 100644
--- a/test/regress/regress0/fp/from_ubv.smt2
+++ b/test/regress/regress0/fp/from_ubv.smt2
@@ -1,3 +1,4 @@
+; REQUIRES: symfpu
 ; EXPECT: unsat
 (set-logic QF_FP)
 (declare-const r RoundingMode)