From 900a7217f8843a17f5ea6bb744b6013f2f394ed7 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Wed, 7 Oct 2020 17:20:52 -0700 Subject: fix unit failures on debug without symfpu (#5212) The following tests fail (locally) when compiling with debug and without symfpu: unit/api/sort_black (Failed) unit/theory/logic_info_white (Failed) unit/util/floatingpoint_black (Child aborted) This PR conditions the relevant parts of these tests to the availability of symfpu. Co-authored-by: Aina Niemetz --- test/unit/api/sort_black.h | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) (limited to 'test/unit/api') diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h index 53563f833..e9f0e04ea 100644 --- a/test/unit/api/sort_black.h +++ b/test/unit/api/sort_black.h @@ -17,6 +17,7 @@ #include #include "api/cvc4cpp.h" +#include "base/configuration.h" using namespace CVC4::api; @@ -271,18 +272,24 @@ void SortBlack::testGetBVSize() void SortBlack::testGetFPExponentSize() { - Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - TS_ASSERT_THROWS_NOTHING(fpSort.getFPExponentSize()); - Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - TS_ASSERT_THROWS(setSort.getFPExponentSize(), CVC4ApiException&); + if (CVC4::Configuration::isBuiltWithSymFPU()) + { + Sort fpSort = d_solver.mkFloatingPointSort(4, 8); + TS_ASSERT_THROWS_NOTHING(fpSort.getFPExponentSize()); + Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); + TS_ASSERT_THROWS(setSort.getFPExponentSize(), CVC4ApiException&); + } } void SortBlack::testGetFPSignificandSize() { - Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - TS_ASSERT_THROWS_NOTHING(fpSort.getFPSignificandSize()); - Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - TS_ASSERT_THROWS(setSort.getFPSignificandSize(), CVC4ApiException&); + if (CVC4::Configuration::isBuiltWithSymFPU()) + { + Sort fpSort = d_solver.mkFloatingPointSort(4, 8); + TS_ASSERT_THROWS_NOTHING(fpSort.getFPSignificandSize()); + Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); + TS_ASSERT_THROWS(setSort.getFPSignificandSize(), CVC4ApiException&); + } } void SortBlack::testGetDatatypeParamSorts() -- cgit v1.2.3