diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-03-23 22:58:31 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-03-23 22:58:31 -0700 |
| commit | c6e9766a910509583a32e85ad8be55aea550c17c (patch) | |
| tree | c0ebc74885920980f0295bdf36cd27308acb9582 /test/unit | |
| parent | 9b7ba1603b2d6ff4c13182655ca8af32966570aa (diff) | |
BV: Fix typerules for rotate operators. (#2895)
Diffstat (limited to 'test/unit')
| -rw-r--r-- | test/unit/api/solver_black.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index dfd92a8c5..c17e23f05 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -451,6 +451,8 @@ void SolverBlack::testMkOpTerm() // mkOpTerm(Kind kind, uint32_t arg) TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(DIVISIBLE_OP, 1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(BITVECTOR_ROTATE_LEFT_OP, 1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(BITVECTOR_ROTATE_RIGHT_OP, 1)); TS_ASSERT_THROWS(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 1), CVC4ApiException&); |