diff options
| author | Tim King <taking@cs.nyu.edu> | 2013-11-19 20:57:15 -0500 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2013-11-20 15:37:18 -0500 |
| commit | bd8e9319aab69db90692f72bc52288329879eefc (patch) | |
| tree | 7bfee530c06836827378fd5b9bd1f47bb4f1eea1 /test/unit | |
| parent | f806a8eedf01753116c225b4c1a5e29543fda370 (diff) | |
Changing the number of bits allocated per field in node values.
Diffstat (limited to 'test/unit')
| -rw-r--r-- | test/unit/expr/expr_manager_public.h | 3 | ||||
| -rw-r--r-- | test/unit/expr/node_manager_black.h | 3 | ||||
| -rw-r--r-- | test/unit/expr/node_manager_white.h | 4 |
3 files changed, 7 insertions, 3 deletions
diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h index d5929a266..204f1bcd2 100644 --- a/test/unit/expr/expr_manager_public.h +++ b/test/unit/expr/expr_manager_public.h @@ -105,7 +105,8 @@ public: void testMkAssociative3() { try { - unsigned int numVars = d_exprManager->maxArity(AND) + 1; + //unsigned int numVars = d_exprManager->maxArity(AND) + 1; + unsigned int numVars = (1<<16) + 1; std::vector<Expr> vars = mkVars(d_exprManager->booleanType(), numVars); Expr n = d_exprManager->mkAssociative(AND,vars); checkAssociative(n,AND,numVars); diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h index 860dfb1a9..4c2cc97e2 100644 --- a/test/unit/expr/node_manager_black.h +++ b/test/unit/expr/node_manager_black.h @@ -314,8 +314,9 @@ public: std::vector<Node> vars; const unsigned int max = metakind::getUpperBoundForKind(AND); TypeNode boolType = d_nodeManager->booleanType(); + Node skolem = d_nodeManager->mkSkolem("i", boolType); for( unsigned int i = 0; i <= max; ++i ) { - vars.push_back( d_nodeManager->mkSkolem("i", boolType) ); + vars.push_back( skolem ); } TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, vars), AssertionException ); #endif diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h index 26872846e..b272cb692 100644 --- a/test/unit/expr/node_manager_white.h +++ b/test/unit/expr/node_manager_white.h @@ -69,8 +69,10 @@ public: TS_ASSERT_THROWS_NOTHING(nb.realloc(20000)); TS_ASSERT_THROWS_NOTHING(nb.realloc(60000)); TS_ASSERT_THROWS_NOTHING(nb.realloc(65535)); + TS_ASSERT_THROWS_NOTHING(nb.realloc(65536)); + TS_ASSERT_THROWS_NOTHING(nb.realloc(67108863)); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(nb.realloc(65536), AssertionException); + TS_ASSERT_THROWS(nb.realloc(67108863), AssertionException); #endif /* CVC4_ASSERTIONS */ } }; |