From 7d27cae34c7c3cda9a7827754fb5b8e485d515db Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 11 Apr 2019 13:06:08 -0500
Subject: [PATCH]  Eliminate Boolean ITE within terms, fixes 2947 (#2949)

---
 src/smt/term_formula_removal.cpp        | 18 ++++++++++++------
 test/regress/CMakeLists.txt             |  1 +
 test/regress/regress0/uf/issue2947.smt2 | 11 +++++++++++
 3 files changed, 24 insertions(+), 6 deletions(-)
 create mode 100644 test/regress/regress0/uf/issue2947.smt2

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index ff17c5622..f610cc7df 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -84,9 +84,13 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
   TypeNode nodeType = node.getType();
   Node skolem;
   Node newAssertion;
-  if(node.getKind() == kind::ITE) {
-    // If an ITE, replace it
-    if (!nodeType.isBoolean() && (!inQuant || !expr::hasBoundVar(node)))
+  // Handle non-Boolean ITEs here. Boolean ones (within terms) are handled
+  // in the "non-variable Boolean term within term" case below.
+  if (node.getKind() == kind::ITE && !nodeType.isBoolean())
+  {
+    // Here, we eliminate the ITE if we are not Boolean and if we do not contain
+    // a bound variable.
+    if (!inQuant || !expr::hasBoundVar(node))
     {
       skolem = getSkolemForNode(node);
       if (skolem.isNull())
@@ -163,13 +167,15 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
            && inTerm
            && !inQuant)
   {
-    // if a non-variable Boolean term, replace it
+    // if a non-variable Boolean term within another term, replace it
     skolem = getSkolemForNode(node);
     if (skolem.isNull())
     {
       // Make the skolem to represent the Boolean term
-      // skolem = nodeManager->mkSkolem("termBT", nodeType, "a variable
-      // introduced due to Boolean term removal");
+      // Skolems introduced for Boolean formulas appearing in terms have a
+      // special kind (BOOLEAN_TERM_VARIABLE) that ensures they are handled
+      // properly in theory combination. We must use this kind here instead of a
+      // generic skolem.
       skolem = nodeManager->mkBooleanTermVariable();
       d_skolem_cache.insert(node, skolem);
 
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 64da9ec61..687dfc6f2 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -933,6 +933,7 @@ set(regress_0_tests
   regress0/uf/euf_simp12.smt
   regress0/uf/euf_simp13.smt
   regress0/uf/iso_brn001.smt
+  regress0/uf/issue2947.smt2
   regress0/uf/pred.smt
   regress0/uf/simple.01.cvc
   regress0/uf/simple.02.cvc
diff --git a/test/regress/regress0/uf/issue2947.smt2 b/test/regress/regress0/uf/issue2947.smt2
new file mode 100644
index 000000000..6bb60b9d7
--- /dev/null
+++ b/test/regress/regress0/uf/issue2947.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_UF)
+(set-info :status unsat)
+(declare-fun f (Bool) Bool)
+(assert
+  (not (f true))
+)
+(assert
+  (f (ite (f true) true (f false)))
+)
+(check-sat)
+(exit)
-- 
2.30.2