diff options
Diffstat (limited to 'src/theory/uf/equality_engine.cpp')
| -rw-r--r-- | src/theory/uf/equality_engine.cpp | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 693b7bd66..b6896e45d 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -81,6 +81,11 @@ void EqualityEngine::init() { Debug("equality") << "EqualityEdge::EqualityEngine(): edge_null = " << +null_edge << std::endl; Debug("equality") << "EqualityEdge::EqualityEngine(): trigger_null = " << +null_trigger << std::endl; + // If we are not at level zero when we initialize this equality engine, we + // may remove true/false from the equality engine when we pop to level zero, + // which leads to issues. + Assert(d_context->getLevel() == 0); + d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); |