From 81544bb6de5b21db7ed5e41d56277105bbea103d Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Tue, 3 Aug 2021 18:41:04 -0700 Subject: [PATCH] Add IEEE-BV-to-FP to external-to-internal mapping in C++ API (#6951) Without this, you can't make terms with that kind. --- src/api/cpp/cvc5.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 69aa720ea..22690fe49 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -241,6 +241,8 @@ const static std::unordered_map s_kinds{ {FLOATINGPOINT_ISPOS, cvc5::Kind::FLOATINGPOINT_ISPOS}, {FLOATINGPOINT_TO_FP_FLOATINGPOINT, cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT}, + {FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, + cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR}, {FLOATINGPOINT_TO_FP_REAL, cvc5::Kind::FLOATINGPOINT_TO_FP_REAL}, {FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR}, -- 2.30.2