diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-01 15:44:34 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-01 20:44:34 +0000 |
| commit | 71699a551d207ab373c733d8ea83a5b071ed99ee (patch) | |
| tree | 639bf606f8374d2685e72919a48b4749088a3a43 /test/unit | |
| parent | 78bfaf2c35fa3b4c7ff35b0b9a5fd0c8c7c5a922 (diff) | |
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.
Diffstat (limited to 'test/unit')
| -rw-r--r-- | test/unit/api/sort_black.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
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()); } |