diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-15 09:35:27 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-15 09:35:27 -0600 |
| commit | 829b3c2798c1f2c0bb313d7eff2c1e76f0184ae2 (patch) | |
| tree | 6855fbf1b5bf7b11958a222f70e9301156931c0b /test/unit/util/array_store_all_white.cpp | |
| parent | 9aeb23f2ae58e4f6dd2b53dbb47cf8c173e56d83 (diff) | |
| parent | 94c4d5b54e7840fa36d76e7c3d52e19c31a1dbc1 (diff) | |
Merge branch 'master' into refactorEagerSolverrefactorEagerSolver
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 |