SyGuS instantiation quantifiers module (#3910)

1 files changed, 9 insertions, 6 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp
index 9d20e1c3c..388234ec2 100644
--- a/src/theory/quantifiers/sygus/sygus_invariance.cpp
+++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp
@@ -92,13 +92,16 @@ void EquivSygusInvarianceTest::init(
   // compute the current examples
   d_bvr = bvr;
   Assert(tds != nullptr);
-  ExampleEvalCache* eec = aconj->getExampleEvalCache(e);
-  if (eec != nullptr)
+  if (aconj != nullptr)
   {
-    // get the result of evaluating bvr on the examples of enumerator e.
-    eec->evaluateVec(bvr, d_exo, false);
-    d_conj = aconj;
-    d_enum = e;
+    ExampleEvalCache* eec = aconj->getExampleEvalCache(e);
+    if (eec != nullptr)
+    {
+      // get the result of evaluating bvr on the examples of enumerator e.
+      eec->evaluateVec(bvr, d_exo, false);
+      d_conj = aconj;
+      d_enum = e;
+    }
   }
 }