diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-08-08 17:08:50 -0700 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2019-08-13 14:25:58 -0700 |
commit | 0ff8f1bf279bcf4b673c5783a7a8b8744667676e (patch) | |
tree | 9007e94e869febf2a6cab0555db3f982b8665f1b /test | |
parent | 018c4f199032d42e4b6f679c5ebf247a0310e3c5 (diff) |
New C++ API: Fix test names of solver_black unit test. (#3170)
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/api/solver_black.h | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 3782b900a..37eccb94c 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -52,7 +52,7 @@ class SolverBlack : public CxxTest::TestSuite void testMkAbstractValue(); void testMkBitVector(); void testMkBoolean(); - void testMkBoundVar(); + void testMkConst(); void testMkEmptySet(); void testMkFalse(); void testMkFloatingPoint(); @@ -295,7 +295,7 @@ void SolverBlack::testMkBitVector() "0bin00001111"); } -void SolverBlack::testMkBoundVar() +void SolverBlack::testMkVar() { Sort boolSort = d_solver->getBooleanSort(); Sort intSort = d_solver->getIntegerSort(); @@ -734,7 +734,7 @@ void SolverBlack::testMkUniverseSet() TS_ASSERT_THROWS_NOTHING(d_solver->mkUniverseSet(d_solver->getBooleanSort())); } -void SolverBlack::testMkVar() +void SolverBlack::testMkConst() { Sort boolSort = d_solver->getBooleanSort(); Sort intSort = d_solver->getIntegerSort(); @@ -797,8 +797,8 @@ void SolverBlack::testDefineFun() Term b11 = d_solver->mkVar(bvSort, "b1"); Term b2 = d_solver->mkVar(d_solver->getIntegerSort(), "b2"); Term b3 = d_solver->mkVar(funSort2, "b3"); - Term v1 = d_solver->mkVar(bvSort, "v1"); - Term v2 = d_solver->mkVar(d_solver->getIntegerSort(), "v2"); + Term v1 = d_solver->mkConst(bvSort, "v1"); + Term v2 = d_solver->mkConst(d_solver->getIntegerSort(), "v2"); Term v3 = d_solver->mkConst(funSort2, "v3"); Term f1 = d_solver->mkConst(funSort1, "f1"); Term f2 = d_solver->mkConst(funSort2, "f2"); @@ -829,8 +829,8 @@ void SolverBlack::testDefineFunRec() Term b11 = d_solver->mkVar(bvSort, "b1"); Term b2 = d_solver->mkVar(d_solver->getIntegerSort(), "b2"); Term b3 = d_solver->mkVar(funSort2, "b3"); - Term v1 = d_solver->mkVar(bvSort, "v1"); - Term v2 = d_solver->mkVar(d_solver->getIntegerSort(), "v2"); + Term v1 = d_solver->mkConst(bvSort, "v1"); + Term v2 = d_solver->mkConst(d_solver->getIntegerSort(), "v2"); Term v3 = d_solver->mkConst(funSort2, "v3"); Term f1 = d_solver->mkConst(funSort1, "f1"); Term f2 = d_solver->mkConst(funSort2, "f2"); @@ -864,8 +864,8 @@ void SolverBlack::testDefineFunsRec() Term b2 = d_solver->mkVar(d_solver->getIntegerSort(), "b2"); Term b3 = d_solver->mkVar(funSort2, "b3"); Term b4 = d_solver->mkVar(uSort, "b4"); - Term v1 = d_solver->mkVar(bvSort, "v1"); - Term v2 = d_solver->mkVar(d_solver->getIntegerSort(), "v2"); + Term v1 = d_solver->mkConst(bvSort, "v1"); + Term v2 = d_solver->mkConst(d_solver->getIntegerSort(), "v2"); Term v3 = d_solver->mkConst(funSort2, "v3"); Term v4 = d_solver->mkConst(uSort, "v4"); Term f1 = d_solver->mkConst(funSort1, "f1"); |