From 9f6da05263951ee353ae587565d0d7f38ef97867 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 21 May 2022 18:23:56 -0500 Subject: [PATCH] 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. --- src/prop/skolem_def_manager.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/prop/skolem_def_manager.cpp b/src/prop/skolem_def_manager.cpp index 013a6f023..b2fca3cdb 100644 --- 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); } } -- 2.30.2