summaryrefslogtreecommitdiff
path: root/src/theory/fp/fp_converter.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/fp/fp_converter.cpp')
-rw-r--r--src/theory/fp/fp_converter.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index c767014cb..0d1b25549 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -1102,7 +1102,7 @@ Node FpConverter::convert(TNode node)
}
break;
- case kind::FLOATINGPOINT_PLUS:
+ case kind::FLOATINGPOINT_ADD:
case kind::FLOATINGPOINT_SUB:
case kind::FLOATINGPOINT_MULT:
case kind::FLOATINGPOINT_DIV:
@@ -1134,7 +1134,7 @@ Node FpConverter::convert(TNode node)
switch (current.getKind())
{
- case kind::FLOATINGPOINT_PLUS:
+ case kind::FLOATINGPOINT_ADD:
d_fpMap.insert(current,
symfpu::add<traits>(fpt(current.getType()),
(*mode).second,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback