Significant revision to theory/arith. The new draft has a lot of small bug fixes and organizational changes. The theory is now enabled to perform checking in the TheoryEngine. This draft can now solve 2 new regression tests test/regress/regress0/ineq_slack.smt and test/regress/regress0/ineq_basic.smt. There is also a small bug fix inside src/expr/attribute.h.

1 files changed, 24 insertions, 0 deletions

diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 7e034036a..52a324d53 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -561,4 +561,28 @@ public:
     sstr << Node::setdepth(3) << o;
     TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
   }
+
+//  This Test is designed to fail in a way that will cause a segfault,
+//  so it is commented out.
+//  This is for demonstrating what a certain type of user error looks like.
+//   Node level0(){
+//     NodeBuilder<> nb(kind::AND);
+//     Node x = d_nodeManager->mkVar(*d_booleanType);
+//     nb << x;
+//     nb << x;
+//     return Node(nb.constructNode());
+//   }
+
+//   TNode level1(){
+//     return level0();
+//   }
+
+//   void testChaining() {
+//     Node res = level1();
+
+//     TS_ASSERT(res.getKind() == kind::NULL_EXPR);
+//     TS_ASSERT(res != Node::null());
+
+//     cerr << "I finished both tests now watch as I crash" << endl;
+//   }
 };