diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-01-07 09:02:02 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-01-07 09:02:02 -0800 |
| commit | 1f6fb54967659ff2ee3f8c29a8d306499fcf1299 (patch) | |
| tree | 4ebdd4569230e55882ccbc61cb8b8f6ef3bb89ff /test/unit | |
| parent | 610952322417e3758f2b62300f618721c269b2b3 (diff) | |
New C++ API: Add missing getType() calls to kick off type checking. (#2773)
Diffstat (limited to 'test/unit')
| -rw-r--r-- | test/unit/api/solver_black.h | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 40f641cbd..5c2c7a8f5 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -288,7 +288,8 @@ void SolverBlack::testMkConst() // mkConst(Kind kind, Sort arg) const TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(EMPTYSET, Sort())); - TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(UNIVERSE_SET, d_solver.mkSetSort(d_solver.getBooleanSort()))); + TS_ASSERT_THROWS_NOTHING(d_solver.mkConst( + UNIVERSE_SET, d_solver.mkSetSort(d_solver.getBooleanSort()))); TS_ASSERT_THROWS(d_solver.mkConst(EMPTYSET, d_solver.getBooleanSort()), CVC4ApiException&); TS_ASSERT_THROWS(d_solver.mkTerm(UNIVERSE_SET, Sort()), CVC4ApiException&); |