Added test/regress/boolean.cvc

diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am
index c5e6ec67688c2ad25e34736f3a9fe50355ed599c..ba7fd1309c13c341ab6e3c1b199cd681a4dfb630 100644 (file)
--- a/test/regress/Makefile.am
+++ b/test/regress/Makefile.am
@@ -33,5 +33,6 @@ TESTS = \
        bmc-ibm-12.smt \
        bmc-ibm-13.smt \
        wiki.cvc \
-       logops.cvc
+       logops.cvc \
+       comb2.shuffled-as.sat03-420.smt
 

diff --git a/test/regress/Makefile.in b/test/regress/Makefile.in
index 2670ecd657463002e2ac8f0bd91315c39a47794a..0db9d000412f3b08502cca3cd985c2b33a376474 100644 (file)
--- a/test/regress/Makefile.in
+++ b/test/regress/Makefile.in
@@ -227,7 +227,8 @@ TESTS = \
        bmc-ibm-12.smt \
        bmc-ibm-13.smt \
        wiki.cvc \
-       logops.cvc
+       logops.cvc \
+       comb2.shuffled-as.sat03-420.smt
 
 all: all-am
 

diff --git a/test/regress/boolean.cvc b/test/regress/boolean.cvc
new file mode 100644 (file)
index 0000000..ac98857
--- /dev/null
+++ b/test/regress/boolean.cvc
@@ -0,0 +1,809 @@
+%% Regression level = 1
+%% Result = Valid
+%% Runtime = 1
+%% Language = presentation
+p : BOOLEAN;
+q : BOOLEAN;
+r : BOOLEAN;
+s : BOOLEAN;
+t : BOOLEAN;
+u : BOOLEAN;
+v : BOOLEAN;
+P1 : BOOLEAN;
+P2 : BOOLEAN;
+P3 : BOOLEAN;
+P4 : BOOLEAN;
+P6 : BOOLEAN;
+P5 : BOOLEAN;
+a41 : BOOLEAN = 
+        IF p THEN FALSE
+        ELSE TRUE
+        ENDIF;
+a42 : BOOLEAN = 
+        IF a41 THEN FALSE
+        ELSE TRUE
+        ENDIF;
+a45 : BOOLEAN = 
+        IF p THEN p
+        ELSE a41
+        ENDIF;
+a46 : BOOLEAN = 
+        IF q THEN FALSE
+        ELSE TRUE
+        ENDIF;
+a49 : BOOLEAN = 
+        IF s THEN t
+        ELSE FALSE
+        ENDIF;
+a58 : BOOLEAN = 
+        IF q THEN q
+        ELSE a46
+        ENDIF;
+a59 : BOOLEAN = 
+        IF r THEN FALSE
+        ELSE TRUE
+        ENDIF;
+a61 : BOOLEAN = 
+        IF s THEN FALSE
+        ELSE TRUE
+        ENDIF;
+a62 : BOOLEAN = 
+        IF s THEN s
+        ELSE a61
+        ENDIF;
+a65 : BOOLEAN = 
+        IF t THEN FALSE
+        ELSE TRUE
+        ENDIF;
+a67 : BOOLEAN = 
+        IF u THEN FALSE
+        ELSE TRUE
+        ENDIF;
+a73 : BOOLEAN = 
+        IF p THEN q
+        ELSE FALSE
+        ENDIF;
+a74 : BOOLEAN = 
+        IF q THEN p
+        ELSE FALSE
+        ENDIF;
+a77 : BOOLEAN = 
+        IF r THEN TRUE
+        ELSE s
+        ENDIF;
+a78 : BOOLEAN = 
+        IF s THEN TRUE
+        ELSE r
+        ENDIF;
+a81 : BOOLEAN = 
+        IF t THEN u
+        ELSE a67
+        ENDIF;
+a82 : BOOLEAN = 
+        IF u THEN t
+        ELSE a65
+        ENDIF;
+a88 : BOOLEAN = 
+        IF q THEN r
+        ELSE FALSE
+        ENDIF;
+a89 : BOOLEAN = 
+        IF p THEN a88
+        ELSE FALSE
+        ENDIF;
+a92 : BOOLEAN = 
+        IF s THEN TRUE
+        ELSE t
+        ENDIF;
+a94 : BOOLEAN = 
+        IF t THEN TRUE
+        ELSE u
+        ENDIF;
+a95 : BOOLEAN = 
+        IF s THEN TRUE
+        ELSE a94
+        ENDIF;
+a105 : BOOLEAN = 
+        IF t THEN u
+        ELSE FALSE
+        ENDIF;
+a111 : BOOLEAN = 
+        IF p THEN q
+        ELSE TRUE
+        ENDIF;
+a112 : BOOLEAN = 
+        IF q THEN r
+        ELSE TRUE
+        ENDIF;
+a114 : BOOLEAN = 
+        IF p THEN r
+        ELSE TRUE
+        ENDIF;
+a116 : BOOLEAN = 
+        IF s THEN t
+        ELSE a65
+        ENDIF;
+a121 : BOOLEAN = 
+        IF a46 THEN a41
+        ELSE TRUE
+        ENDIF;
+a126 : BOOLEAN = 
+        IF a59 THEN a61
+        ELSE 
+          IF a61 THEN FALSE
+          ELSE TRUE
+          ENDIF
+        ENDIF;
+a130 : BOOLEAN = 
+        IF q THEN TRUE
+        ELSE r
+        ENDIF;
+a132 : BOOLEAN = 
+        IF p THEN r
+        ELSE FALSE
+        ENDIF;
+a133 : BOOLEAN = 
+        IF a73 THEN TRUE
+        ELSE a132
+        ENDIF;
+a138 : BOOLEAN = 
+        IF a92 THEN 
+          IF s THEN TRUE
+          ELSE u
+          ENDIF
+        ELSE FALSE
+        ENDIF;
+a143 : BOOLEAN = 
+        IF a114 THEN a112
+        ELSE FALSE
+        ENDIF;
+a145 : BOOLEAN = 
+        IF 
+          IF 
+            IF p THEN TRUE
+            ELSE q
+            ENDIF THEN r
+          ELSE TRUE
+          ENDIF THEN a143
+        ELSE 
+          IF a143 THEN FALSE
+          ELSE TRUE
+          ENDIF
+        ENDIF;
+a147 : BOOLEAN = 
+        IF s THEN t
+        ELSE TRUE
+        ENDIF;
+a148 : BOOLEAN = 
+        IF s THEN u
+        ELSE TRUE
+        ENDIF;
+a149 : BOOLEAN = 
+        IF a147 THEN TRUE
+        ELSE a148
+        ENDIF;
+a153 : BOOLEAN = 
+        IF a73 THEN r
+        ELSE TRUE
+        ENDIF;
+a154 : BOOLEAN = 
+        IF a114 THEN TRUE
+        ELSE a112
+        ENDIF;
+a158 : BOOLEAN = 
+        IF a147 THEN a148
+        ELSE FALSE
+        ENDIF;
+a162 : BOOLEAN = 
+        IF p THEN a112
+        ELSE TRUE
+        ENDIF;
+a167 : BOOLEAN = 
+        IF a46 THEN TRUE
+        ELSE a59
+        ENDIF;
+a171 : BOOLEAN = 
+        IF a61 THEN a65
+        ELSE FALSE
+        ENDIF;
+a176 : BOOLEAN = 
+        IF p THEN q
+        ELSE r
+        ENDIF;
+a178 : BOOLEAN = 
+        IF p THEN a46
+        ELSE a59
+        ENDIF;
+a183 : BOOLEAN = 
+        IF s THEN a65
+        ELSE 
+          IF a65 THEN FALSE
+          ELSE TRUE
+          ENDIF
+        ENDIF;
+a187 : BOOLEAN = 
+        IF a41 THEN TRUE
+        ELSE q
+        ENDIF;
+a192 : BOOLEAN = 
+        IF 
+          IF r THEN s
+          ELSE FALSE
+          ENDIF THEN TRUE
+        ELSE 
+          IF a59 THEN t
+          ELSE FALSE
+          ENDIF
+        ENDIF;
+a197 : BOOLEAN = 
+        IF a111 THEN 
+          IF a41 THEN r
+          ELSE TRUE
+          ENDIF
+        ELSE FALSE
+        ENDIF;
+a200 : BOOLEAN = 
+        IF a49 THEN TRUE
+        ELSE a171
+        ENDIF;
+a204 : BOOLEAN = 
+        IF p THEN q
+        ELSE a46
+        ENDIF;
+a205 : BOOLEAN = 
+        IF q THEN p
+        ELSE TRUE
+        ENDIF;
+a206 : BOOLEAN = 
+        IF a111 THEN a205
+        ELSE FALSE
+        ENDIF;
+a210 : BOOLEAN = 
+        IF p THEN a46
+        ELSE TRUE
+        ENDIF;
+a214 : BOOLEAN = 
+        IF a73 THEN FALSE
+        ELSE TRUE
+        ENDIF;
+a221 : BOOLEAN = 
+        IF 
+          IF p THEN a46
+          ELSE FALSE
+          ENDIF THEN r
+        ELSE TRUE
+        ENDIF;
+a225 : BOOLEAN = 
+        IF a187 THEN a132
+        ELSE TRUE
+        ENDIF;
+a228 : BOOLEAN = 
+        IF q THEN r
+        ELSE a59
+        ENDIF;
+a231 : BOOLEAN = 
+        IF a204 THEN r
+        ELSE a59
+        ENDIF;
+a237 : BOOLEAN = 
+        IF q THEN a132
+        ELSE 
+          IF a41 THEN s
+          ELSE FALSE
+          ENDIF
+        ENDIF;
+a288 : BOOLEAN = 
+        IF 
+          IF 
+            IF p THEN a41
+            ELSE a42
+            ENDIF THEN FALSE
+          ELSE TRUE
+          ENDIF THEN 
+          IF 
+            IF a45 THEN 
+              IF 
+                IF q THEN TRUE
+                ELSE a46
+                ENDIF THEN 
+                IF 
+                  IF r THEN r
+                  ELSE TRUE
+                  ENDIF THEN 
+                  IF 
+                    IF a49 THEN s
+                    ELSE TRUE
+                    ENDIF THEN 
+                    IF u THEN 
+                      IF u THEN TRUE
+                      ELSE v
+                      ENDIF
+                    ELSE TRUE
+                    ENDIF
+                  ELSE FALSE
+                  ENDIF
+                ELSE FALSE
+                ENDIF
+              ELSE FALSE
+              ENDIF
+            ELSE FALSE
+            ENDIF THEN 
+            IF 
+              IF a58 THEN 
+                IF 
+                  IF r THEN r
+                  ELSE a59
+                  ENDIF THEN a62
+                ELSE FALSE
+                ENDIF
+              ELSE FALSE
+              ENDIF THEN 
+              IF 
+                IF a45 THEN 
+                  IF a62 THEN 
+                    IF 
+                      IF t THEN t
+                      ELSE a65
+                      ENDIF THEN 
+                      IF a67 THEN a67
+                      ELSE 
+                        IF a67 THEN FALSE
+                        ELSE TRUE
+                        ENDIF
+                      ENDIF
+                    ELSE FALSE
+                    ENDIF
+                  ELSE FALSE
+                  ENDIF
+                ELSE FALSE
+                ENDIF THEN 
+                IF 
+                  IF 
+                    IF a73 THEN a74
+                    ELSE 
+                      IF a74 THEN FALSE
+                      ELSE TRUE
+                      ENDIF
+                    ENDIF THEN 
+                    IF 
+                      IF a77 THEN a78
+                      ELSE 
+                        IF a78 THEN FALSE
+                        ELSE TRUE
+                        ENDIF
+                      ENDIF THEN 
+                      IF a81 THEN a82
+                      ELSE 
+                        IF a82 THEN FALSE
+                        ELSE TRUE
+                        ENDIF
+                      ENDIF
+                    ELSE FALSE
+                    ENDIF
+                  ELSE FALSE
+                  ENDIF THEN 
+                  IF 
+                    IF 
+                      IF 
+                        IF a73 THEN r
+                        ELSE FALSE
+                        ENDIF THEN a89
+                      ELSE 
+                        IF a89 THEN FALSE
+                        ELSE TRUE
+                        ENDIF
+                      ENDIF THEN 
+                      IF 
+                        IF a92 THEN TRUE
+                        ELSE u
+                        ENDIF THEN a95
+                      ELSE 
+                        IF a95 THEN FALSE
+                        ELSE TRUE
+                        ENDIF
+                      ENDIF
+                    ELSE FALSE
+                    ENDIF THEN 
+                    IF 
+                      IF 
+                        IF 
+                          IF p THEN p
+                          ELSE FALSE
+                          ENDIF THEN p
+                        ELSE a41
+                        ENDIF THEN 
+                        IF 
+                          IF 
+                            IF q THEN TRUE
+                            ELSE q
+                            ENDIF THEN q
+                          ELSE a46
+                          ENDIF THEN 
+                          IF 
+                            IF 
+                              IF r THEN a77
+                              ELSE FALSE
+                              ENDIF THEN r
+                            ELSE a59
+                            ENDIF THEN 
+                            IF 
+                              IF t THEN TRUE
+                              ELSE a105
+                              ENDIF THEN t
+                            ELSE a65
+                            ENDIF
+                          ELSE FALSE
+                          ENDIF
+                        ELSE FALSE
+                        ENDIF
+                      ELSE FALSE
+                      ENDIF THEN 
+                      IF a58 THEN 
+                        IF 
+                          IF 
+                            IF 
+                              IF a111 THEN a112
+                              ELSE FALSE
+                              ENDIF THEN a114
+                            ELSE TRUE
+                            ENDIF THEN 
+                            IF 
+                              IF a116 THEN a81
+                              ELSE FALSE
+                              ENDIF THEN 
+                              IF s THEN u
+                              ELSE a67
+                              ENDIF
+                            ELSE TRUE
+                            ENDIF
+                          ELSE FALSE
+                          ENDIF THEN 
+                          IF 
+                            IF 
+                              IF a111 THEN a121
+                              ELSE 
+                                IF a121 THEN FALSE
+                                ELSE TRUE
+                                ENDIF
+                              ENDIF THEN 
+                              IF 
+                                IF r THEN s
+                                ELSE a61
+                                ENDIF THEN a126
+                              ELSE 
+                                IF a126 THEN FALSE
+                                ELSE TRUE
+                                ENDIF
+                              ENDIF
+                            ELSE FALSE
+                            ENDIF THEN 
+                            IF 
+                              IF 
+                                IF 
+                                  IF p THEN a130
+                                  ELSE FALSE
+                                  ENDIF THEN a133
+                                ELSE 
+                                  IF a133 THEN FALSE
+                                  ELSE TRUE
+                                  ENDIF
+                                ENDIF THEN 
+                                IF 
+                                  IF s THEN TRUE
+                                  ELSE a105
+                                  ENDIF THEN a138
+                                ELSE 
+                                  IF a138 THEN FALSE
+                                  ELSE TRUE
+                                  ENDIF
+                                ENDIF
+                              ELSE FALSE
+                              ENDIF THEN 
+                              IF 
+                                IF a145 THEN 
+                                  IF 
+                                    IF s THEN a94
+                                    ELSE TRUE
+                                    ENDIF THEN a149
+                                  ELSE 
+                                    IF a149 THEN FALSE
+                                    ELSE TRUE
+                                    ENDIF
+                                  ENDIF
+                                ELSE FALSE
+                                ENDIF THEN 
+                                IF 
+                                  IF 
+                                    IF a153 THEN a154
+                                    ELSE 
+                                      IF a154 THEN FALSE
+                                      ELSE TRUE
+                                      ENDIF
+                                    ENDIF THEN 
+                                    IF 
+                                      IF s THEN a105
+                                      ELSE TRUE
+                                      ENDIF THEN a158
+                                    ELSE 
+                                      IF a158 THEN FALSE
+                                      ELSE TRUE
+                                      ENDIF
+                                    ENDIF
+                                  ELSE FALSE
+                                  ENDIF THEN 
+                                  IF 
+                                    IF a153 THEN a162
+                                    ELSE 
+                                      IF a162 THEN FALSE
+                                      ELSE TRUE
+                                      ENDIF
+                                    ENDIF THEN 
+                                    IF 
+                                      IF 
+                                        IF a42 THEN p
+                                        ELSE a41
+                                        ENDIF THEN 
+                                        IF 
+                                          IF 
+                                            IF a88 THEN FALSE
+                                            ELSE TRUE
+                                            ENDIF THEN a167
+                                          ELSE 
+                                            IF a167 THEN FALSE
+                                            ELSE TRUE
+                                            ENDIF
+                                          ENDIF THEN 
+                                          IF 
+                                            IF a92 THEN FALSE
+                                            ELSE TRUE
+                                            ENDIF THEN a171
+                                          ELSE 
+                                            IF a171 THEN FALSE
+                                            ELSE TRUE
+                                            ENDIF
+                                          ENDIF
+                                        ELSE FALSE
+                                        ENDIF
+                                      ELSE FALSE
+                                      ENDIF THEN 
+                                      IF 
+                                        IF 
+                                          IF 
+                                            IF a176 THEN FALSE
+                                            ELSE TRUE
+                                            ENDIF THEN a178
+                                          ELSE 
+                                            IF a178 THEN FALSE
+                                            ELSE TRUE
+                                            ENDIF
+                                          ENDIF THEN 
+                                          IF 
+                                            IF a116 THEN FALSE
+                                            ELSE TRUE
+                                            ENDIF THEN a183
+                                          ELSE 
+                                            IF a183 THEN FALSE
+                                            ELSE TRUE
+                                            ENDIF
+                                          ENDIF
+                                        ELSE FALSE
+                                        ENDIF THEN 
+                                        IF 
+                                          IF 
+                                            IF a111 THEN a187
+                                            ELSE 
+                                              IF a187 THEN FALSE
+                                              ELSE TRUE
+                                              ENDIF
+                                            ENDIF THEN 
+                                            IF 
+                                              IF r THEN s
+                                              ELSE t
+                                              ENDIF THEN a192
+                                            ELSE 
+                                              IF a192 THEN FALSE
+                                              ELSE TRUE
+                                              ENDIF
+                                            ENDIF
+                                          ELSE FALSE
+                                          ENDIF THEN 
+                                          IF 
+                                            IF 
+                                              IF a176 THEN a197
+                                              ELSE 
+                                                IF a197 THEN FALSE
+                                                ELSE TRUE
+                                                ENDIF
+                                              ENDIF THEN 
+                                              IF a116 THEN a200
+                                              ELSE 
+                                                IF a200 THEN FALSE
+                                                ELSE TRUE
+                                                ENDIF
+                                              ENDIF
+                                            ELSE FALSE
+                                            ENDIF THEN 
+                                            IF 
+                                              IF a204 THEN a206
+                                              ELSE 
+                                                IF a206 THEN FALSE
+                                                ELSE TRUE
+                                                ENDIF
+                                              ENDIF THEN 
+                                              IF 
+                                                IF a111 THEN TRUE
+                                                ELSE a205
+                                                ENDIF THEN 
+                                                IF 
+                                                  IF a46 THEN TRUE
+                                                  ELSE 
+                                                    IF 
+                                                      IF a210 THEN p
+                                                      ELSE FALSE
+                                                      ENDIF THEN FALSE
+                                                    ELSE TRUE
+                                                    ENDIF
+                                                  ENDIF THEN 
+                                                  IF 
+                                                    IF a210 THEN a214
+                                                    ELSE 
+                                                      IF a214 THEN FALSE
+                                                      ELSE TRUE
+                                                      ENDIF
+                                                    ENDIF THEN 
+                                                    IF a145 THEN 
+                                                      IF 
+                                                        IF a162 THEN a153
+                                                        ELSE 
+                                                          IF a153 THEN FALSE
+                                                          ELSE TRUE
+                                                          ENDIF
+                                                        ENDIF THEN 
+                                                        IF 
+                                                          IF 
+                                                            IF p THEN a130
+                                                            ELSE TRUE
+                                                            ENDIF THEN a221
+                                                          ELSE 
+                                                            IF a221 THEN FALSE
+                                                            ELSE TRUE
+                                                            ENDIF
+                                                          ENDIF THEN 
+                                                          IF 
+                                                            IF 
+                                                              IF p THEN a112
+                                                              ELSE FALSE
+                                                              ENDIF THEN a225
+                                                            ELSE 
+                                                              IF a225 THEN FALSE
+                                                              ELSE TRUE
+                                                              ENDIF
+                                                            ENDIF THEN 
+                                                            IF 
+                                                              IF 
+                                                                IF p THEN a228
+                                                                ELSE 
+                                                                  IF a228 THEN FALSE
+                                                                  ELSE TRUE
+                                                                  ENDIF
+                                                                ENDIF THEN a231
+                                                              ELSE 
+                                                                IF a231 THEN FALSE
+                                                                ELSE TRUE
+                                                                ENDIF
+                                                              ENDIF THEN 
+                                                              IF 
+                                                                IF 
+                                                                  IF p THEN a88
+                                                                  ELSE 
+                                                                    IF a46 THEN s
+                                                                    ELSE FALSE
+                                                                    ENDIF
+                                                                  ENDIF THEN a237
+                                                                ELSE 
+                                                                  IF a237 THEN FALSE
+                                                                  ELSE TRUE
+                                                                  ENDIF
+                                                                ENDIF THEN 
+                                                                IF 
+                                                                  IF 
+                                                                    IF P1 THEN 
+                                                                      IF P2 THEN TRUE
+                                                                      ELSE P3
+                                                                      ENDIF
+                                                                    ELSE 
+                                                                      IF P3 THEN TRUE
+                                                                      ELSE P4
+                                                                      ENDIF
+                                                                    ENDIF THEN 
+                                                                    IF 
+                                                                      IF P3 THEN 
+                                                                        IF P6 THEN FALSE
+                                                                        ELSE TRUE
+                                                                        ENDIF
+                                                                      ELSE 
+                                                                        IF P4 THEN P1
+                                                                        ELSE TRUE
+                                                                        ENDIF
+                                                                      ENDIF THEN 
+                                                                      IF 
+                                                                        IF 
+                                                                          IF P2 THEN P5
+                                                                          ELSE FALSE
+                                                                          ENDIF THEN FALSE
+                                                                        ELSE TRUE
+                                                                        ENDIF THEN 
+                                                                        IF P2 THEN P5
+                                                                        ELSE TRUE
+                                                                        ENDIF
+                                                                      ELSE FALSE
+                                                                      ENDIF
+                                                                    ELSE FALSE
+                                                                    ENDIF
+                                                                  ELSE FALSE
+                                                                  ENDIF THEN 
+                                                                  IF 
+                                                                    IF P3 THEN P6
+                                                                    ELSE TRUE
+                                                                    ENDIF THEN FALSE
+                                                                  ELSE TRUE
+                                                                  ENDIF
+                                                                ELSE TRUE
+                                                                ENDIF
+                                                              ELSE FALSE
+                                                              ENDIF
+                                                            ELSE FALSE
+                                                            ENDIF
+                                                          ELSE FALSE
+                                                          ENDIF
+                                                        ELSE FALSE
+                                                        ENDIF
+                                                      ELSE FALSE
+                                                      ENDIF
+                                                    ELSE FALSE
+                                                    ENDIF
+                                                  ELSE FALSE
+                                                  ENDIF
+                                                ELSE FALSE
+                                                ENDIF
+                                              ELSE FALSE
+                                              ENDIF
+                                            ELSE FALSE
+                                            ENDIF
+                                          ELSE FALSE
+                                          ENDIF
+                                        ELSE FALSE
+                                        ENDIF
+                                      ELSE FALSE
+                                      ENDIF
+                                    ELSE FALSE
+                                    ENDIF
+                                  ELSE FALSE
+                                  ENDIF
+                                ELSE FALSE
+                                ENDIF
+                              ELSE FALSE
+                              ENDIF
+                            ELSE FALSE
+                            ENDIF
+                          ELSE FALSE
+                          ENDIF
+                        ELSE FALSE
+                        ENDIF
+                      ELSE FALSE
+                      ENDIF
+                    ELSE FALSE
+                    ENDIF
+                  ELSE FALSE
+                  ENDIF
+                ELSE FALSE
+                ENDIF
+              ELSE FALSE
+              ENDIF
+            ELSE FALSE
+            ENDIF
+          ELSE FALSE
+          ENDIF
+        ELSE FALSE
+        ENDIF;
+QUERY a288;

diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index aa99c70c42f091101de0d94deda2ce0baab27fe0..c5a2bb609af53362ec88c332108997e0eb787a03 100644 (file)
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -15,18 +15,42 @@
 
 #include <cxxtest/TestSuite.h>
 
+#include "expr/node_manager.h"
 #include "expr/node.h"
 
 using namespace CVC4;
+using namespace std;
 
 class NodeBlack : public CxxTest::TestSuite {
+private:
+
+  NodeManagerScope *d_scope;
+  NodeManager *d_nm;
+
 public:
 
-  void testNull() {
-    Node::null();
+  void setUp() {
+    d_nm = new NodeManager();
+    d_scope = new NodeManagerScope(d_nm);
+  }
+
+  void tearDown(){
+    delete d_nm;
+    delete d_scope;
   }
 
-  void testCopyCtor() {
-    Node e(Node::null());
+  void testEqExpr(){
+    /*Node eqExpr(const Node& right) const;*/
+    Node left = d_nm->mkNode(TRUE);
+    Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE)));
+
+    Node eq = left.eqExpr(right);
+
+    Node first = *(eq.begin());
+    Node second = *(eq.begin()++);
+
+    TS_ASSERT(first.getKind() == NULL);
+    TS_ASSERT(second.getKind() == NULL);
   }
+
 };