From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Fri, 11 May 2018 01:43:09 +0000 (-0500)
Subject: Also exclude ITEs from ITE conditions in SygusUnifStrat (#1903)
X-Git-Tag: cvc5-1.0.0~5063
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f50620d05f8c661a0adf34d8ad2a41782d546396;p=cvc5.git

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 32af47c81..855922fc5 100644
--- 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;