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 | |
| parent | 9c0b0f4c42619d1de116dc73f2c5111fd27ea85c (diff) | |
Fixing test failures in production build
Diffstat (limited to 'test')
| -rw-r--r-- | test/unit/Makefile.am | 2 | ||||
| -rw-r--r-- | test/unit/expr/node_manager_black.h | 6 |
2 files changed, 7 insertions, 1 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index c48afc10d..dc203061c 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -1,7 +1,7 @@ # All unit tests UNIT_TESTS = \ expr/expr_public \ - expr/expr_manager_public \ + expr/expr_manager_public \ expr/node_white \ expr/node_black \ expr/kind_black \ 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 } }; |