diff options
Diffstat (limited to 'src/theory/quantifiers')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_io.cpp | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 61916ce4c..e330a8476 100644 --- 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()) |