Eagerly ensure literal on active guards for sygus enumerators (#2531)

diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index a10ecc56610fda316778f3311b1598312a915bef..18e9619cbb88e712d5e5423cc30f9334f33e1d91 100644 (file)
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -482,7 +482,10 @@ void TermDbSygus::registerEnumerator(Node e,
   NodeManager* nm = NodeManager::currentNM();
   if( mkActiveGuard ){
     // make the guard
-    d_enum_to_active_guard[e] = nm->mkSkolem("eG", nm->booleanType());
+    Node ag = nm->mkSkolem("eG", nm->booleanType());
+    // must ensure it is a literal immediately here
+    ag = d_quantEngine->getValuation().ensureLiteral(ag);
+    d_enum_to_active_guard[e] = ag;
   }
 
   Trace("sygus-db") << "  registering symmetry breaking clauses..."