pow2 -- final changes (#6800)

[cvc5.git] / src / theory / arith / congruence_manager.cpp

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 96272f939c0e8d71fc22a89018dbbe9ef7c9b7dd..9e7202f1dfdb238ba7277d36b5a9d25dee7783f9 100644 (file)
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -85,6 +85,7 @@ void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee,
   d_ee->addFunctionKind(kind::EXPONENTIAL);
   d_ee->addFunctionKind(kind::SINE);
   d_ee->addFunctionKind(kind::IAND);
+  d_ee->addFunctionKind(kind::POW2);
   // have proof equality engine only if proofs are enabled
   Assert(isProofEnabled() == (pfee != nullptr));
   d_pfee = pfee;