Fix side condition check in sygus core connective (#3600)

1 files changed, 4 insertions, 0 deletions

diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index a8c4cb0d1..a924873d0 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -805,6 +805,10 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
           scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end());
           scasserts.push_back(d_sc);
           std::shuffle(scasserts.begin(), scasserts.end(), Random::getRandom());
+          for (const Node& sca : scasserts)
+          {
+            checkSc.assertFormula(sca.toExpr());
+          }
           Result rsc = checkSc.checkSat();
           Trace("sygus-ccore")
               << "----- check-sat returned " << rsc << std::endl;