1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index 472a82e29..e4c23977e 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -996,6 +996,10 @@ bool SygusEnumerator::TermEnumMasterInterp::initialize(SygusEnumerator* se,
 Node SygusEnumerator::TermEnumMasterInterp::getCurrent() { return *d_te; }
 bool SygusEnumerator::TermEnumMasterInterp::increment()
 {
+  if (d_te.isFinished())
+  {
+    return false;
+  }
   SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn];
   Node curr = getCurrent();
   tc.addTerm(curr);