Ensure lemmas from sygus repair const are guarded (#3385)

1 files changed, 6 insertions, 3 deletions

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index c319d7a37..96f347890 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -247,9 +247,11 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums,
             enums[i], enum_values[i], exp);
       }
       Assert(!exp.empty());
-      Node expn =
-          exp.size() == 1 ? exp[0] : NodeManager::currentNM()->mkNode(AND, exp);
-      lems.push_back(expn.negate());
+      NodeManager* nm = NodeManager::currentNM();
+      Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
+      // must guard it
+      expn = nm->mkNode(OR, d_parent->getGuard().negate(), expn.negate());
+      lems.push_back(expn);
       return false;
     }
   }
@@ -300,6 +302,7 @@ bool Cegis::processConstructCandidates(const std::vector<Node>& enums,
 
 void Cegis::addRefinementLemma(Node lem)
 {
+  Trace("cegis-rl") << "Cegis::addRefinementLemma: " << lem << std::endl;
   d_refinement_lemmas.push_back(lem);
   // apply existing substitution
   Node slem = lem;