From 0ff8f1bf279bcf4b673c5783a7a8b8744667676e Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 8 Aug 2019 17:08:50 -0700 Subject: [PATCH] New C++ API: Fix test names of solver_black unit test. (#3170) --- test/unit/api/solver_black.h | 18 +++++++++--------- 1 file 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"); -- 2.30.2