From 71699a551d207ab373c733d8ea83a5b071ed99ee Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 1 Apr 2021 15:44:34 -0500 Subject: Fix type rule for to_real (#6257) This fixes the type rule for to_real to match SMT-LIB: its argument must be an integer. This required fixing the TPTP parser which has a more relaxed semantics for to_real / to_rat. This also fixes Solver::isReal, which should return false if we are the integer type. Fixes #6208. --- test/unit/api/sort_black.cpp | 2 ++ 1 file changed, 2 insertions(+) (limited to 'test') diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp index e0507e749..fa4b1cc9d 100644 --- a/test/unit/api/sort_black.cpp +++ b/test/unit/api/sort_black.cpp @@ -71,12 +71,14 @@ TEST_F(TestApiBlackSort, isBoolean) TEST_F(TestApiBlackSort, isInteger) { ASSERT_TRUE(d_solver.getIntegerSort().isInteger()); + ASSERT_TRUE(!d_solver.getRealSort().isInteger()); ASSERT_NO_THROW(Sort().isInteger()); } TEST_F(TestApiBlackSort, isReal) { ASSERT_TRUE(d_solver.getRealSort().isReal()); + ASSERT_TRUE(!d_solver.getIntegerSort().isReal()); ASSERT_NO_THROW(Sort().isReal()); } -- cgit v1.2.3