Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.

22 files changed, 361 insertions, 18 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 20de7a97c..1e533cc61 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -177,7 +177,9 @@ BUG_TESTS = \
 	bug595.cvc \
 	bug596.cvc \
 	bug596b.cvc \
-	bug605.cvc
+	bug605.cvc \
+	bt-test-00.smt2 \
+	bt-test-01.smt2
 #bug590.smt2
 
 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am
index b974bc95e..17cfa3fd4 100644
--- a/test/regress/regress0/arrays/Makefile.am
+++ b/test/regress/regress0/arrays/Makefile.am
@@ -49,7 +49,8 @@ TESTS =	\
 	constarr2.cvc \
 	constarr3.cvc \
 	parsing_ringer.cvc \
-	bug637.delta.smt2
+	bug637.delta.smt2 \
+	bool-array.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/arrays/bool-array.smt2 b/test/regress/regress0/arrays/bool-array.smt2
new file mode 100644
index 000000000..f05d0266b
--- /dev/null
+++ b/test/regress/regress0/arrays/bool-array.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores
+; EXPECT: unsat
+(set-logic QF_AX)
+(set-info :status unsat)
+
+(declare-fun a () (Array Bool Bool))
+(declare-fun b () (Array Bool Bool))
+
+(assert (not (= (select a (= a b)) (select a (not (= a b))))))
+(assert (= (select a true) (select a false)))
+
+(check-sat)
+
diff --git a/test/regress/regress0/bt-test-00.smt2 b/test/regress/regress0/bt-test-00.smt2
new file mode 100644
index 000000000..cd3e1137e
--- /dev/null
+++ b/test/regress/regress0/bt-test-00.smt2
@@ -0,0 +1,22 @@
+; COMMAND-LINE: --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_UF)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+
+(declare-fun f (Bool) Bool)
+(declare-fun g (Bool) Bool)
+(declare-fun h (Bool) Bool)
+
+(declare-fun x () Bool)
+(declare-fun y () Bool)
+(declare-fun z () Bool)
+
+(assert (not (= (f x) (f y))))
+(assert (not (= (g y) (g z))))
+(assert (not (= (h z) (h x))))
+
+(check-sat)
+
+(exit)
diff --git a/test/regress/regress0/bt-test-01.smt2 b/test/regress/regress0/bt-test-01.smt2
new file mode 100644
index 000000000..918dcf9ec
--- /dev/null
+++ b/test/regress/regress0/bt-test-01.smt2
@@ -0,0 +1,27 @@
+; COMMAND-LINE: --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_UF)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+
+(declare-fun x0 () Bool)
+(declare-fun y0 () Bool)
+(declare-fun z0 () Bool)
+
+(assert (or x0 y0))
+(assert (or (not y0) z0))
+
+(declare-fun x1 () Bool)
+(declare-fun y1 () Bool)
+
+(assert x1)
+(assert y1)
+
+(declare-fun f (Bool) Bool)
+
+(assert (not (= (f (or x0 z0)) (f (and x1 y1)))))
+
+(check-sat)
+
+(exit)
diff --git a/test/regress/regress0/bug217.smt2 b/test/regress/regress0/bug217.smt2
index a1e29f63e..34cfcad33 100644
--- a/test/regress/regress0/bug217.smt2
+++ b/test/regress/regress0/bug217.smt2
@@ -1,6 +1,7 @@
+; COMMAND-LINE: --no-check-proofs
 ; EXPECT: unsat
 (set-logic QF_UF)
-(set-info :status sat)
+(set-info :status unsat)
 (set-option :produce-models true)
 (declare-fun f (Bool) Bool)
 (declare-fun x () Bool)
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index a8a637377..fed65924b 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -71,7 +71,10 @@ TESTS =	\
 	coda_simp_model.smt2 \
 	Test1-tup-mp.cvc \
 	dt-param-card4-unsat.smt2 \
-	dt-param-card4-bool-sat.smt2
+	dt-param-card4-bool-sat.smt2 \
+	bug604.smt2 \
+	bug597-rbt.smt2 \
+	example-dailler-min.smt2
 
 FAILING_TESTS = \
 	datatype-dump.cvc
diff --git a/test/regress/regress0/datatypes/bug597-rbt.smt2 b/test/regress/regress0/datatypes/bug597-rbt.smt2
new file mode 100644
index 000000000..45d82a522
--- /dev/null
+++ b/test/regress/regress0/datatypes/bug597-rbt.smt2
@@ -0,0 +1,12 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+
+; Tree type
+(declare-datatypes () ((Tree (node (data Int) (color Bool) (left Tree) (right Tree)) (nil))))
+
+; content function
+(declare-fun size (Tree) Int)
+(assert (= (size nil) 0))
+
+
+(check-sat)
diff --git a/test/regress/regress0/datatypes/bug604.smt2 b/test/regress/regress0/datatypes/bug604.smt2
new file mode 100644
index 000000000..15a60c3e3
--- /dev/null
+++ b/test/regress/regress0/datatypes/bug604.smt2
@@ -0,0 +1,9 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-datatypes () ( (PairIntInt (pair (firstPairIntInt Int)
+(secondPairIntInt Int)) ) ))
+(declare-fun /ArrayIntOfPair () (Array Int PairIntInt))
+(declare-datatypes () ( (SequenceABC (sequenceABC (a Int) (b Bool) (c Int)) )
+))
+(declare-fun /ArrayIntOfSequenceABC () (Array Int SequenceABC))
+(check-sat)
diff --git a/test/regress/regress0/datatypes/example-dailler-min.smt2 b/test/regress/regress0/datatypes/example-dailler-min.smt2
new file mode 100644
index 000000000..1698fc3b0
--- /dev/null
+++ b/test/regress/regress0/datatypes/example-dailler-min.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes () ((D (C (R Bool)))))
+(declare-fun a () (Array Int D))
+(declare-fun P ((Array Int D)) Bool)
+(assert (P a))
+(check-sat)
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index af8776ace..79cff2947 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -65,7 +65,9 @@ TESTS =	\
 	memory_model-R_cpp-dd.cvc \
 	bug764.smt2 \
 	ko-bound-set.cvc \
-	cons-sets-bounds.smt2
+	cons-sets-bounds.smt2 \
+	bug651.smt2 \
+	bug652.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/fmf/bug651.smt2 b/test/regress/regress0/fmf/bug651.smt2
new file mode 100644
index 000000000..9afc47972
--- /dev/null
+++ b/test/regress/regress0/fmf/bug651.smt2
@@ -0,0 +1,43 @@
+; COMMAND-LINE: --fmf-fun --no-check-models
+; EXPECT: sat
+(set-logic UFDTSLIA)
+(set-info :smt-lib-version 2.5)
+(set-option :produce-models true)
+
+(declare-datatypes () (
+    (Conditional_Int (Conditional_Int$CAbsent_Int) (Conditional_Int$CPresent_Int (Conditional_Int$CPresent_Int$value Int)))
+    (Conditional_T_titleType (Conditional_T_titleType$CAbsent_T_titleType) (Conditional_T_titleType$CPresent_T_titleType (Conditional_T_titleType$CPresent_T_titleType$value T_titleType)))
+    (Conditional_boolean (Conditional_boolean$CAbsent_boolean) (Conditional_boolean$CPresent_boolean (Conditional_boolean$CPresent_boolean$value Bool)))
+    (Conditional_string (Conditional_string$CAbsent_string) (Conditional_string$CPresent_string (Conditional_string$CPresent_string$value String)))
+    (Double (Double$CINF) (Double$CNINF) (Double$CNaN) (Double$CValue (Double$CValue$value Int)))
+    (List_T_titleType (List_T_titleType$CNil_T_titleType) (List_T_titleType$Cstr_T_titleType (List_T_titleType$Cstr_T_titleType$head T_titleType) (List_T_titleType$Cstr_T_titleType$tail List_T_titleType)))
+    (List_boolean (List_boolean$CNil_boolean) (List_boolean$Cstr_boolean (List_boolean$Cstr_boolean$head Bool) (List_boolean$Cstr_boolean$tail List_boolean)))
+    (List_string (List_string$CNil_string) (List_string$Cstr_string (List_string$Cstr_string$head String) (List_string$Cstr_string$tail List_string)))
+    (T_titleType (T_titleType$C_T_titleType (T_titleType$C_T_titleType$base String)))
+) )
+
+(define-fun f1361$isValid_string((x String)) Bool true)
+(define-fun f5131$isValid_T_titleType((x T_titleType)) Bool (and (f1361$isValid_string (T_titleType$C_T_titleType$base x)) (<= (str.len (T_titleType$C_T_titleType$base x)) 80)))
+(define-funs-rec
+  (
+    (f5242$isValidElementsList_T_titleType((x List_T_titleType)) Bool)
+  )
+  (
+    (=> (is-List_T_titleType$Cstr_T_titleType x) (and (f5131$isValid_T_titleType (List_T_titleType$Cstr_T_titleType$head x)) (f5242$isValidElementsList_T_titleType (List_T_titleType$Cstr_T_titleType$tail x))))
+  )
+)
+(define-fun f1348$isValid_boolean((x Bool)) Bool true)
+(define-funs-rec
+  (
+    (f4169$isValidElementsList_boolean((x List_boolean)) Bool)
+  )
+  (
+    (=> (is-List_boolean$Cstr_boolean x) (and (f1348$isValid_boolean (List_boolean$Cstr_boolean$head x)) (f4169$isValidElementsList_boolean (List_boolean$Cstr_boolean$tail x))))
+  )
+)
+
+
+(declare-const title T_titleType)
+(check-sat)
+
+
diff --git a/test/regress/regress0/fmf/bug652.smt2 b/test/regress/regress0/fmf/bug652.smt2
new file mode 100644
index 000000000..13748eeea
--- /dev/null
+++ b/test/regress/regress0/fmf/bug652.smt2
@@ -0,0 +1,22 @@
+; COMMAND-LINE: --fmf-fun --no-check-models
+; EXPECT: sat
+(set-logic UFDTSLIA)
+(set-info :smt-lib-version 2.5)
+(set-option :produce-models true)
+
+(declare-datatypes () (
+    (List_boolean (List_boolean$CNil_boolean) (List_boolean$Cstr_boolean (List_boolean$Cstr_boolean$head Bool) (List_boolean$Cstr_boolean$tail List_boolean)))
+) )
+
+(define-funs-rec
+  (
+    (f4208$lengthList_boolean((x List_boolean)) Int)
+  )
+  (
+    (ite (is-List_boolean$CNil_boolean x) 0 (+ 1 (f4208$lengthList_boolean (List_boolean$Cstr_boolean$tail x))))
+  )
+)
+
+
+(declare-const boolean Bool)
+(check-sat)
diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index 99619a6aa..262132779 100644
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -46,7 +46,9 @@ BUG_TESTS = \
   inc-double-u.smt2 \
   fmf-fun-dbu.smt2 \
   inc-define.smt2 \
-  bug765.smt2
+  bug765.smt2 \
+  bug691.smt2 \
+  bug694-Unapply1.scala-0.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/push-pop/bug691.smt2 b/test/regress/regress0/push-pop/bug691.smt2
new file mode 100644
index 000000000..df8964658
--- /dev/null
+++ b/test/regress/regress0/push-pop/bug691.smt2
@@ -0,0 +1,21 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: sat
+(set-logic UFDTSLIA)
+(set-info :smt-lib-version 2.5)
+
+(declare-datatypes () (
+    (Response (Response$Response (Response$Response$success Bool)))
+    ) )
+
+
+(push 1)
+(declare-fun $BLout$3248$0$1$() Response)
+(assert (= $BLout$3248$0$1$ (Response$Response true)))
+(check-sat)
+(pop 1)
+
+(push 1)
+(declare-fun $BLout$3248$2$1$() Response)
+(assert (= $BLout$3248$2$1$ (Response$Response true)))
+(check-sat)
diff --git a/test/regress/regress0/push-pop/bug694-Unapply1.scala-0.smt2 b/test/regress/regress0/push-pop/bug694-Unapply1.scala-0.smt2
new file mode 100644
index 000000000..8fdee6f43
--- /dev/null
+++ b/test/regress/regress0/push-pop/bug694-Unapply1.scala-0.smt2
@@ -0,0 +1,147 @@
+; COMMAND-LINE: --incremental
+; EXPECT: unsat
+; EXPECT: sat
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun start!1 () Bool)
+
+(assert start!1)
+
+(declare-fun b!15 () Bool)
+
+(declare-fun e!22 () Bool)
+
+(declare-fun error_value!0 () Bool)
+
+(assert (=> b!15 (= e!22 error_value!0)))
+
+(declare-fun b!16 () Bool)
+
+(declare-fun e!20 () Bool)
+
+(assert (=> b!16 (= e!20 e!22)))
+
+(declare-fun b!20 () Bool)
+
+(declare-datatypes () ( (Option!3 (None!1) (Some!1 (v!71 tuple2!0)))  (tuple2!0 (tuple2!1 (_1!0 Unit!0) (_2!0 Bool)))  (Unit!0 (Unit!1)) ))
+
+(declare-fun lt!7 () Option!3)
+
+(declare-fun Unit!2 () Unit!0)
+
+(assert (=> b!16 (= b!20 (ite (is-Some!1 lt!7) (= (_1!0 (v!71 lt!7)) Unit!2) false))))
+
+(assert (=> b!16 (or (not b!20) (not b!15))))
+
+(assert (=> b!16 (or b!20 b!15)))
+
+(declare-datatypes () ( (tuple3!0 (tuple3!1 (_1!1 (_ BitVec 32)) (_2!1 Bool) (_3!0 Unit!0))) ))
+
+(declare-fun unapply!2 (tuple3!0) Option!3)
+
+(declare-fun Unit!3 () Unit!0)
+
+(assert (=> b!16 (= lt!7 (unapply!2 (tuple3!1 #x0000002A false Unit!3)))))
+
+(declare-fun b!17 () Bool)
+
+(declare-fun e!21 () Bool)
+
+(assert (=> b!17 e!21))
+
+(declare-fun b!18 () Bool)
+
+(declare-fun Unit!4 () Unit!0)
+
+(assert (=> b!18 (= e!20 (_2!0 (v!71 (unapply!2 (tuple3!1 #x0000002A false Unit!4)))))))
+
+(declare-fun lt!6 () Bool)
+
+(assert (=> start!1 (not lt!6)))
+
+(assert (=> start!1 (= lt!6 e!20)))
+
+(assert (=> start!1 (= b!18 e!21)))
+
+(assert (=> start!1 (or (not b!18) (not b!16))))
+
+(assert (=> start!1 (or b!18 b!16)))
+
+(declare-fun b!19 () Bool)
+
+(assert (=> (and start!1 (not b!19)) (not e!21)))
+
+(declare-fun lt!8 () Option!3)
+
+(assert (=> start!1 (= b!19 (ite (is-Some!1 lt!8) true false))))
+
+(declare-fun Unit!5 () Unit!0)
+
+(assert (=> start!1 (= lt!8 (unapply!2 (tuple3!1 #x0000002A false Unit!5)))))
+
+(assert (=> (and b!19 (not b!17)) (not e!21)))
+
+(declare-fun Unit!6 () Unit!0)
+
+(assert (=> b!19 (= b!17 (_2!0 (v!71 (unapply!2 (tuple3!1 #x0000002A false Unit!6)))))))
+
+(declare-fun Unit!7 () Unit!0)
+
+(assert (=> b!20 (= e!22 (_2!0 (v!71 (unapply!2 (tuple3!1 #x0000002A false Unit!7)))))))
+
+(push 1)
+
+(assert (and (and (and (and (not b!19) (not start!1)) (not b!20)) (not b!18)) (not b!16)))
+
+(check-sat)
+
+(pop 1)
+
+(push 1)
+
+(assert true)
+
+(check-sat)
+
+(pop 1)
+
+(declare-fun d!1 () Bool)
+
+(declare-fun e!25 () Bool)
+
+(assert (=> d!1 e!25))
+
+(declare-fun b!23 () Bool)
+
+(assert (=> (and d!1 (not b!23)) (not e!25)))
+
+(declare-fun Unit!8 () Unit!0)
+
+(declare-fun Unit!9 () Unit!0)
+
+(declare-fun Unit!10 () Unit!0)
+
+(declare-fun Unit!11 () Unit!0)
+
+(assert (=> d!1 (= b!23 (= (unapply!2 (tuple3!1 #x0000002A false Unit!8)) (ite (= (_1!1 (tuple3!1 #x0000002A false Unit!9)) #x00000000) None!1 (Some!1 (tuple2!1 (_3!0 (tuple3!1 #x0000002A false Unit!10)) (_2!1 (tuple3!1 #x0000002A false Unit!11)))))))))
+
+(assert (=> b!23 (= e!25 true)))
+
+(assert (=> b!18 d!1))
+
+(assert (=> start!1 d!1))
+
+(assert (=> b!16 d!1))
+
+(assert (=> b!20 d!1))
+
+(assert (=> b!19 d!1))
+
+(push 1)
+
+(assert true)
+
+(check-sat)
+
+(pop 1)
+
diff --git a/test/regress/regress0/quantifiers/small-bug1-fixpoint-3.smt2 b/test/regress/regress0/quantifiers/small-bug1-fixpoint-3.smt2
index da48f5e68..c26cde173 100644
--- a/test/regress/regress0/quantifiers/small-bug1-fixpoint-3.smt2
+++ b/test/regress/regress0/quantifiers/small-bug1-fixpoint-3.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --cbqi-all --no-check-models
 ; EXPECT: sat
+;AJR:BROKEN
 (set-logic UFBV)
 (set-info :status sat)
 (declare-fun Verilog__main.impl_PC_valid_64_1_39_!3 (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool) Bool)
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index 91b276889..8a4ce33b7 100644
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -50,7 +50,8 @@ TESTS =	\
 	cnf-iff-base.smt2 \
 	cnf-ite.smt2 \
 	cnf-and-neg.smt2 \
-	cnf_abc.smt2
+	cnf_abc.smt2 \
+	bool-pred-nested.smt2
 
 EXTRA_DIST = $(TESTS) \
 	mkpidgeon
diff --git a/test/regress/regress0/uf/bool-pred-nested.smt2 b/test/regress/regress0/uf/bool-pred-nested.smt2
new file mode 100644
index 000000000..66275423e
--- /dev/null
+++ b/test/regress/regress0/uf/bool-pred-nested.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_UF)
+(set-info :status sat)
+(declare-fun P (Bool Bool) Bool)
+
+(assert (P (P true (P false false)) (P false true)))
+
+(check-sat)
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index eb0ff3ad3..bd00b770f 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -346,14 +346,14 @@ public:
   }
 
   void testIffNode() {
-    /*  Node iffNode(const Node& right) const; */
+    /*  Node eqNode(const Node& right) const; */
 
     Node left = d_nodeManager->mkConst(true);
     Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
-    Node eq = left.iffNode(right);
+    Node eq = left.eqNode(right);
 
 
-    TS_ASSERT(IFF == eq.getKind());
+    TS_ASSERT(EQUAL == eq.getKind());
     TS_ASSERT(2   == eq.getNumChildren());
 
     TS_ASSERT(*(eq.begin()) == left);
@@ -398,8 +398,8 @@ public:
     Node n = d_nodeManager->mkNode(NOT, a);
     TS_ASSERT(NOT == n.getKind());
 
-    n = d_nodeManager->mkNode(IFF, a, b);
-    TS_ASSERT(IFF == n.getKind());
+    n = d_nodeManager->mkNode(EQUAL, a, b);
+    TS_ASSERT(EQUAL == n.getKind());
 
     Node x = d_nodeManager->mkSkolem("x", *d_realType);
     Node y = d_nodeManager->mkSkolem("y", *d_realType);
diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index c93accd33..7a6281e5b 100644
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -178,7 +178,7 @@ class CnfStreamWhite : public CxxTest::TestSuite {
         d_nodeManager->mkNode(
             kind::IMPLIES, d_nodeManager->mkNode(kind::AND, a, b),
             d_nodeManager->mkNode(
-                kind::IFF, d_nodeManager->mkNode(kind::OR, c, d),
+                kind::EQUAL, d_nodeManager->mkNode(kind::OR, c, d),
                 d_nodeManager->mkNode(kind::NOT,
                                       d_nodeManager->mkNode(kind::XOR, e, f)))),
         false, false, RULE_INVALID, Node::null());
@@ -203,7 +203,7 @@ class CnfStreamWhite : public CxxTest::TestSuite {
     NodeManagerScope nms(d_nodeManager);
     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::IFF, a, b), false,
+    d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::EQUAL, a, b), false,
                                   false, RULE_INVALID, Node::null());
     TS_ASSERT(d_satSolver->addClauseCalled());
   }
diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h
index cb5e20db9..e5c18ff83 100644
--- a/test/unit/util/boolean_simplification_black.h
+++ b/test/unit/util/boolean_simplification_black.h
@@ -94,10 +94,10 @@ public:
     hfc = d_nm->mkNode(kind::APPLY_UF, h, fc);
     gfb = d_nm->mkNode(kind::APPLY_UF, g, fb);
 
-    ac = d_nm->mkNode(kind::IFF, a, c);
-    ffbd = d_nm->mkNode(kind::IFF, ffb, d);
-    efhc = d_nm->mkNode(kind::IFF, e, fhc);
-    dfa = d_nm->mkNode(kind::IFF, d, fa);
+    ac = d_nm->mkNode(kind::EQUAL, a, c);
+    ffbd = d_nm->mkNode(kind::EQUAL, ffb, d);
+    efhc = d_nm->mkNode(kind::EQUAL, e, fhc);
+    dfa = d_nm->mkNode(kind::EQUAL, d, fa);
 
     // this test is designed for >= 10 removal threshold
     TS_ASSERT_LESS_THAN_EQUALS(10u,