diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-06-02 10:16:26 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-02 17:16:26 +0000 |
| commit | dde15bdbf752246fe7cb504df22261e0ad3835db (patch) | |
| tree | ff0b646059dc67c68e24abcc3af5fb3ceeabdc41 /test/unit/api | |
| parent | 338982182dbdabecf6f3b06e659621cf43bed916 (diff) | |
Remove redundant logic ALL_SUPPORTED. (#6664)
Diffstat (limited to 'test/unit/api')
| -rw-r--r-- | test/unit/api/solver_black.cpp | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index bc8f3ed74..018207293 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -1552,7 +1552,7 @@ TEST_F(TestApiBlackSolver, getQuantifierEliminationDisjunct) TEST_F(TestApiBlackSolver, declareSeparationHeap) { - d_solver.setLogic("ALL_SUPPORTED"); + d_solver.setLogic("ALL"); Sort integer = d_solver.getIntegerSort(); ASSERT_NO_THROW(d_solver.declareSeparationHeap(integer, integer)); // cannot declare separation logic heap more than once @@ -1592,7 +1592,7 @@ TEST_F(TestApiBlackSolver, getSeparationHeapTerm1) TEST_F(TestApiBlackSolver, getSeparationHeapTerm2) { - d_solver.setLogic("ALL_SUPPORTED"); + d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); d_solver.setOption("produce-models", "false"); checkSimpleSeparationConstraints(&d_solver); @@ -1601,7 +1601,7 @@ TEST_F(TestApiBlackSolver, getSeparationHeapTerm2) TEST_F(TestApiBlackSolver, getSeparationHeapTerm3) { - d_solver.setLogic("ALL_SUPPORTED"); + d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); d_solver.setOption("produce-models", "true"); Term t = d_solver.mkFalse(); @@ -1612,7 +1612,7 @@ TEST_F(TestApiBlackSolver, getSeparationHeapTerm3) TEST_F(TestApiBlackSolver, getSeparationHeapTerm4) { - d_solver.setLogic("ALL_SUPPORTED"); + d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); d_solver.setOption("produce-models", "true"); Term t = d_solver.mkTrue(); @@ -1623,7 +1623,7 @@ TEST_F(TestApiBlackSolver, getSeparationHeapTerm4) TEST_F(TestApiBlackSolver, getSeparationHeapTerm5) { - d_solver.setLogic("ALL_SUPPORTED"); + d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); d_solver.setOption("produce-models", "true"); checkSimpleSeparationConstraints(&d_solver); @@ -1642,7 +1642,7 @@ TEST_F(TestApiBlackSolver, getSeparationNilTerm1) TEST_F(TestApiBlackSolver, getSeparationNilTerm2) { - d_solver.setLogic("ALL_SUPPORTED"); + d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); d_solver.setOption("produce-models", "false"); checkSimpleSeparationConstraints(&d_solver); @@ -1651,7 +1651,7 @@ TEST_F(TestApiBlackSolver, getSeparationNilTerm2) TEST_F(TestApiBlackSolver, getSeparationNilTerm3) { - d_solver.setLogic("ALL_SUPPORTED"); + d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); d_solver.setOption("produce-models", "true"); Term t = d_solver.mkFalse(); @@ -1662,7 +1662,7 @@ TEST_F(TestApiBlackSolver, getSeparationNilTerm3) TEST_F(TestApiBlackSolver, getSeparationNilTerm4) { - d_solver.setLogic("ALL_SUPPORTED"); + d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); d_solver.setOption("produce-models", "true"); Term t = d_solver.mkTrue(); @@ -1673,7 +1673,7 @@ TEST_F(TestApiBlackSolver, getSeparationNilTerm4) TEST_F(TestApiBlackSolver, getSeparationNilTerm5) { - d_solver.setLogic("ALL_SUPPORTED"); + d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); d_solver.setOption("produce-models", "true"); checkSimpleSeparationConstraints(&d_solver); |