1 files changed, 10 insertions, 5 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 6497bee0b..56edc55c6 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -260,11 +260,16 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
       if (options::sygusUnifCondIndependent() && !unif_enums[1][e].empty())
       {
         Node eu = unif_enums[1][e][0];
-        Node g = d_u_enum_manager.getActiveGuardForEnumerator(eu);
-        Node exp_exc = d_tds->getExplain()
-                           ->getExplanationForEquality(eu, unif_values[1][e][0])
-                           .negate();
-        lems.push_back(nm->mkNode(OR, g.negate(), exp_exc));
+        Assert(d_tds->isEnumerator(eu));
+        if (d_tds->isPassiveEnumerator(eu))
+        {
+          Node g = d_u_enum_manager.getActiveGuardForEnumerator(eu);
+          Node exp_exc =
+              d_tds->getExplain()
+                  ->getExplanationForEquality(eu, unif_values[1][e][0])
+                  .negate();
+          lems.push_back(nm->mkNode(OR, g.negate(), exp_exc));
+        }
       }
     }
   }