diff options
Diffstat (limited to 'test/unit/expr/node_manager_black.h')
| -rw-r--r-- | test/unit/expr/node_manager_black.h | 3 |
1 files changed, 2 insertions, 1 deletions
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 |