Also exclude ITEs from ITE conditions in SygusUnifStrat (#1903)

diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index 32af47c812ff00efe12d1abf2d3a4a311a28f134..855922fc5bd4c60ed76ca8c7ff52139c580cebcb 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -801,7 +801,7 @@ void SygusUnifStrategy::staticLearnRedundantOps(
       if (op.getKind() == kind::BUILTIN)
       {
         Kind k = NodeManager::operatorToKind(op);
-        if (k == NOT || k == OR || k == AND)
+        if (k == NOT || k == OR || k == AND || k == ITE)
         {
           // can eliminate if their argument types are simple loops to this type
           bool type_ok = true;