Fix fast SyGuS enumeration for interpreted constants (#3501)

3 files changed, 49 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);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e7252834e..e4b5b8057 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1736,6 +1736,7 @@ set(regress_1_tests
   regress1/sygus/nia-max-square-ns.sy
   regress1/sygus/no-flat-simp.sy
   regress1/sygus/no-mention.sy
+  regress1/sygus/once_2.sy
   regress1/sygus/only-const-grammar.sy
   regress1/sygus/parity-si-rcons.sy
   regress1/sygus/pbe_multi.sy
diff --git a/test/regress/regress1/sygus/once_2.sy b/test/regress/regress1/sygus/once_2.sy
new file mode 100644
index 000000000..af6d56aaf
--- /dev/null
+++ b/test/regress/regress1/sygus/once_2.sy
@@ -0,0 +1,44 @@
+; EXPECT: unsat
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+(set-logic BV)
+
+(define-sort Stream () (_ BitVec 2))
+
+(define-fun BV_ONE () Stream (_ bv1 2))
+
+(define-fun
+  O ( (X Stream) ) Stream
+  (bvneg (bvand X (bvnot (bvsub X BV_ONE))))
+)
+
+(synth-fun op ((x Stream)) Stream
+  (( y_term Stream))
+  (( y_term Stream (
+    ( Constant Stream)
+    ( Variable Stream)
+    ( bvnot y_term )
+    ( bvand y_term y_term )
+    ( bvor y_term y_term )
+    ( bvneg y_term )
+    ( bvadd y_term y_term )
+    ( bvsub y_term y_term )
+    ( bvmul y_term y_term )
+    ( bvudiv y_term y_term )
+    ( bvurem y_term y_term )
+    ( bvshl y_term y_term )
+    ( bvlshr y_term y_term )
+  ))
+))
+
+(define-fun C ((x Stream)) Bool
+  (= (op x) (O x))
+)
+
+(constraint (and
+(C (_ bv0 2))
+(C (_ bv1 2))
+(C (_ bv2 2))
+(C (_ bv3 2))
+))
+
+(check-synth)