diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2020-10-07 17:20:52 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-07 17:20:52 -0700 |
| commit | 900a7217f8843a17f5ea6bb744b6013f2f394ed7 (patch) | |
| tree | 69a0f3b9373b7deabc253798002577ba530190bd /test/unit/api | |
| parent | 5d51949548af6df9a18f498de2d424f15988a07b (diff) | |
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 <aina.niemetz@gmail.com>
Diffstat (limited to 'test/unit/api')
| -rw-r--r-- | test/unit/api/sort_black.h | 23 |
1 files changed, 15 insertions, 8 deletions
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 <cxxtest/TestSuite.h> #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() |