From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 21 May 2022 23:23:56 +0000 (-0500)
Subject: Reenable assertion in skolem definition manager (#8797)
X-Git-Tag: cvc5-1.0.1~109
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9f6da05263951ee353ae587565d0d7f38ef97867;p=cvc5.git

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 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);
   }
 }