diff options
Diffstat (limited to 'src/api/cpp/cvc5.cpp')
| -rw-r--r-- | src/api/cpp/cvc5.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index c62dde511..9e398b518 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -2908,7 +2908,7 @@ std::int64_t Term::getInt64Value() const CVC5_API_ARG_CHECK_EXPECTED(detail::isInt64(*d_node), *d_node) << "Term to be a 64-bit integer value when calling getInt64Value()"; //////// all checks before this line - return detail::getInteger(*d_node).getLong(); + return detail::getInteger(*d_node).getSigned64(); //////// CVC5_API_TRY_CATCH_END; } @@ -2931,7 +2931,7 @@ std::uint64_t Term::getUInt64Value() const << "Term to be a unsigned 64-bit integer value when calling " "getUInt64Value()"; //////// all checks before this line - return detail::getInteger(*d_node).getUnsignedLong(); + return detail::getInteger(*d_node).getUnsigned64(); //////// CVC5_API_TRY_CATCH_END; } @@ -3029,8 +3029,8 @@ std::pair<std::int64_t, std::uint64_t> Term::getReal64Value() const << "Term to be a 64-bit rational value when calling getReal64Value()"; //////// all checks before this line const Rational& r = detail::getRational(*d_node); - return std::make_pair(r.getNumerator().getLong(), - r.getDenominator().getUnsignedLong()); + return std::make_pair(r.getNumerator().getSigned64(), + r.getDenominator().getUnsigned64()); //////// CVC5_API_TRY_CATCH_END; } |