diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-06-01 21:56:35 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-06-01 21:56:35 +0000 |
commit | 9e28a6013e0c2c926d79254ad1e419228ea4d337 (patch) | |
tree | ea3996937d5b925df6f3def6fce64cc8d300a40e /test/unit/expr/node_manager_black.h | |
parent | 9c0b0f4c42619d1de116dc73f2c5111fd27ea85c (diff) |
Fixing test failures in production build
Diffstat (limited to 'test/unit/expr/node_manager_black.h')
-rw-r--r-- | test/unit/expr/node_manager_black.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h index e3be1bedd..78c38d782 100644 --- a/test/unit/expr/node_manager_black.h +++ b/test/unit/expr/node_manager_black.h @@ -338,13 +338,18 @@ public: } + /* This test is only valid if assertions are enabled. */ void testMkNodeTooFew() { +#ifdef CVC4_ASSERTIONS TS_ASSERT_THROWS( d_nodeManager->mkNode(AND), AssertionException ); Node x = d_nodeManager->mkVar( d_nodeManager->booleanType() ); TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, x), AssertionException ); +#endif } + /* This test is only valid if assertions are enabled. */ void testMkNodeTooMany() { +#ifdef CVC4_ASSERTIONS std::vector<Node> vars; const unsigned int max = metakind::getUpperBoundForKind(AND); TypeNode boolType = d_nodeManager->booleanType(); @@ -352,6 +357,7 @@ public: vars.push_back( d_nodeManager->mkVar(boolType) ); } TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, vars), AssertionException ); +#endif } }; |