summaryrefslogtreecommitdiff
path: root/src/api/cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/api/cpp')
-rw-r--r--src/api/cpp/cvc5.cpp4
-rw-r--r--src/api/cpp/cvc5_kind.h2
2 files changed, 3 insertions, 3 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 436ac9856..16366c3cf 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -216,7 +216,7 @@ const static std::unordered_map<Kind, cvc5::Kind> s_kinds{
{FLOATINGPOINT_EQ, cvc5::Kind::FLOATINGPOINT_EQ},
{FLOATINGPOINT_ABS, cvc5::Kind::FLOATINGPOINT_ABS},
{FLOATINGPOINT_NEG, cvc5::Kind::FLOATINGPOINT_NEG},
- {FLOATINGPOINT_PLUS, cvc5::Kind::FLOATINGPOINT_PLUS},
+ {FLOATINGPOINT_ADD, cvc5::Kind::FLOATINGPOINT_ADD},
{FLOATINGPOINT_SUB, cvc5::Kind::FLOATINGPOINT_SUB},
{FLOATINGPOINT_MULT, cvc5::Kind::FLOATINGPOINT_MULT},
{FLOATINGPOINT_DIV, cvc5::Kind::FLOATINGPOINT_DIV},
@@ -502,7 +502,7 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction>
{cvc5::Kind::FLOATINGPOINT_EQ, FLOATINGPOINT_EQ},
{cvc5::Kind::FLOATINGPOINT_ABS, FLOATINGPOINT_ABS},
{cvc5::Kind::FLOATINGPOINT_NEG, FLOATINGPOINT_NEG},
- {cvc5::Kind::FLOATINGPOINT_PLUS, FLOATINGPOINT_PLUS},
+ {cvc5::Kind::FLOATINGPOINT_ADD, FLOATINGPOINT_ADD},
{cvc5::Kind::FLOATINGPOINT_SUB, FLOATINGPOINT_SUB},
{cvc5::Kind::FLOATINGPOINT_MULT, FLOATINGPOINT_MULT},
{cvc5::Kind::FLOATINGPOINT_DIV, FLOATINGPOINT_DIV},
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 2805f6203..6f6bf1d0e 100644
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -1428,7 +1428,7 @@ enum CVC5_EXPORT Kind : int32_t
* - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
* - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
*/
- FLOATINGPOINT_PLUS,
+ FLOATINGPOINT_ADD,
/**
* Floating-point sutraction.
*
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback