Fixes for corner case of decision tree learning with different types (#4887)

There was a last minute change was a typo when merging 103b5ea .
Also the fix in that commit needed to be slightly more robust to the case when either branch of an ITE had a different sygus type.

Fixes regress1.

diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index 61916ce4c28e3c3b397c253c84ffd03a9e1e535a..e330a84760fc8c21a390273df33e9a810a39c25b 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -58,7 +58,7 @@ bool UnifContextIo::updateContext(SygusUnifIo* sui,
     }
     if (v != poln)
     {
-      if (v == d_true)
+      if (d_vals[i] == d_true)
       {
         d_vals[i] = d_false;
         changed = true;
@@ -1431,9 +1431,12 @@ Node SygusUnifIo::constructSol(
           }
           else
           {
-            // if the child types are different, it could still make a
-            // difference to recurse, for instance see issue #4790.
-            bool childTypesEqual = ce.getType() == etn;
+            // if the branch types are different, it could still make a
+            // difference to recurse, for instance see issue #4790. We do this
+            // if either branch is a different type from the current type.
+            TypeNode branchType1 = etis->d_cenum[1].first.getType();
+            TypeNode branchType2 = etis->d_cenum[2].first.getType();
+            bool childTypesEqual = branchType1 == etn && branchType2 == etn;
             if (!childTypesEqual)
             {
               if (!ecache_child.d_enum_vals.empty())