diff options
Diffstat (limited to 'test/unit/util/array_store_all_white.cpp')
| -rw-r--r-- | test/unit/util/array_store_all_white.cpp | 24 |
1 files changed, 14 insertions, 10 deletions
diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp index 1272926db..887a214dd 100644 --- a/test/unit/util/array_store_all_white.cpp +++ b/test/unit/util/array_store_all_white.cpp @@ -18,6 +18,8 @@ #include "test_smt.h" #include "util/rational.h" +using namespace cvc5::kind; + namespace cvc5 { namespace test { @@ -30,15 +32,15 @@ TEST_F(TestUtilWhiteArrayStoreAll, store_all) TypeNode usort = d_nodeManager->mkSort("U"); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->integerType(), d_nodeManager->realType()), - d_nodeManager->mkConst(Rational(9, 2))); + d_nodeManager->mkConst(CONST_RATIONAL, Rational(9, 2))); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkSort("U"), usort), d_nodeManager->mkConst(UninterpretedConstant(usort, 0))); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8), d_nodeManager->realType()), - d_nodeManager->mkConst(Rational(0))); + d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8), d_nodeManager->integerType()), - d_nodeManager->mkConst(Rational(0))); + d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))); } TEST_F(TestUtilWhiteArrayStoreAll, type_errors) @@ -47,13 +49,14 @@ TEST_F(TestUtilWhiteArrayStoreAll, type_errors) d_nodeManager->mkConst(UninterpretedConstant( d_nodeManager->mkSort("U"), 0))), IllegalArgumentException); - ASSERT_THROW(ArrayStoreAll(d_nodeManager->integerType(), - d_nodeManager->mkConst(Rational(9, 2))), - IllegalArgumentException); + ASSERT_THROW( + ArrayStoreAll(d_nodeManager->integerType(), + d_nodeManager->mkConst(CONST_RATIONAL, Rational(9, 2))), + IllegalArgumentException); ASSERT_THROW( ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->integerType(), d_nodeManager->mkSort("U")), - d_nodeManager->mkConst(Rational(9, 2))), + d_nodeManager->mkConst(CONST_RATIONAL, Rational(9, 2))), IllegalArgumentException); } @@ -70,9 +73,10 @@ TEST_F(TestUtilWhiteArrayStoreAll, const_error) IllegalArgumentException); ASSERT_THROW( ArrayStoreAll(d_nodeManager->integerType(), - d_nodeManager->mkNode(kind::PLUS, - d_nodeManager->mkConst(Rational(1)), - d_nodeManager->mkConst(Rational(0)))), + d_nodeManager->mkNode( + kind::PLUS, + d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)), + d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)))), IllegalArgumentException); } } // namespace test |