summaryrefslogtreecommitdiff
path: root/src/theory/fp/theory_fp.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/fp/theory_fp.cpp')
-rw-r--r--src/theory/fp/theory_fp.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index a48f62c6d..3d81a2995 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -101,7 +101,7 @@ void TheoryFp::finishInit()
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ABS);
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_NEG);
- d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_PLUS);
+ d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ADD);
// d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_SUB); // Removed
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_MULT);
d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_DIV);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback