Reenable assertion in skolem definition manager (#8797)

This reenables a variant of an assertion that was deleted in #8749, a weaker version of that assertion should now hold.

diff --git a/src/prop/skolem_def_manager.cpp b/src/prop/skolem_def_manager.cpp
index 013a6f023abcad02d0471a89cabd8d55ab34cef6..b2fca3cdb9346a1d6f15d16c68a1e9e5f24ff390 100644 (file)
--- a/src/prop/skolem_def_manager.cpp
+++ b/src/prop/skolem_def_manager.cpp
@@ -35,6 +35,11 @@ void SkolemDefManager::notifySkolemDefinition(TNode skolem, Node def)
   // equivalent up to purification
   if (d_skDefs.find(skolem) == d_skDefs.end())
   {
+    // should not have already computed whether the skolem has skolems or
+    // otherwise we should have marked that we have skolems, or else
+    // our computation of hasSkolems is wrong after adding this definition
+    Assert(d_hasSkolems.find(skolem) == d_hasSkolems.end()
+           || d_hasSkolems[skolem]);
     d_skDefs.insert(skolem, def);
   }
 }