diff options
Diffstat (limited to 'test/unit/node/node_manager_white.cpp')
-rw-r--r-- | test/unit/node/node_manager_white.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/test/unit/node/node_manager_white.cpp b/test/unit/node/node_manager_white.cpp index fe06f85d3..64f6a70f5 100644 --- a/test/unit/node/node_manager_white.cpp +++ b/test/unit/node/node_manager_white.cpp @@ -23,6 +23,7 @@ namespace cvc5 { using namespace cvc5::expr; +using namespace cvc5::kind; namespace test { @@ -33,8 +34,8 @@ class TestNodeWhiteNodeManager : public TestNode TEST_F(TestNodeWhiteNodeManager, mkConst_rational) { Rational i("3"); - Node n = d_nodeManager->mkConst(i); - Node m = d_nodeManager->mkConst(i); + Node n = d_nodeManager->mkConst(CONST_RATIONAL, i); + Node m = d_nodeManager->mkConst(CONST_RATIONAL, i); ASSERT_EQ(n.getId(), m.getId()); } |