Minor fix for computing look-ahead conditionals in PBE i/o.

2 files changed, 6 insertions, 2 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index dee9c6e4f..ebde19eac 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -1282,6 +1282,7 @@ Node SygusUnifIo::constructSol(
             {
               if (x.d_uinfo.find(ce) == x.d_uinfo.end())
               {
+                x.d_uinfo[ce].clear();
                 Trace("sygus-sui-dt-debug2")
                     << "  reg : PBE: Look for direct solutions for conditional "
                        "enumerator "
@@ -1352,9 +1353,8 @@ Node SygusUnifIo::constructSol(
               // solved terms in at least one branch
               //    only applicable if we have not modified the return value
               std::map<int, std::vector<Node> > solved_cond;
-              if (!x.isReturnValueModified())
+              if (!x.isReturnValueModified() && !x.d_uinfo[ce].empty())
               {
-                Assert(x.d_uinfo.find(ce) != x.d_uinfo.end());
                 int solve_max = 0;
                 for (Node& cond : itpc->second)
                 {
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h
index f7faab389..90612cfaf 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.h
@@ -143,6 +143,10 @@ class UnifContextIo : public UnifContext
     * pairs.
     */
     std::map<Node, std::map<unsigned, Node>> d_look_ahead_sols;
+    /** clear */
+    void clear() { d_look_ahead_sols.clear(); }
+    /** is empty */
+    bool empty() { return d_look_ahead_sols.empty(); }
   };
   /** map from enumerators to the above info class */
   std::map<Node, UEnumInfo> d_uinfo;