BV: Fix typerules for rotate operators. (#2895)

diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 616a03f6b1ee80e103f15a403a04cfbc8ae753b7..a9509df425d9c597ca0d7e9b56d6fc3967d6b421 100644 (file)
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -348,7 +348,7 @@ class BitVectorRotateLeftOpTypeRule
                                      TNode n,
                                      bool check)
   {
-    Assert(n.getKind() == kind::BITVECTOR_ROTATE_LEFT);
+    Assert(n.getKind() == kind::BITVECTOR_ROTATE_LEFT_OP);
     return nodeManager->builtinOperatorType();
   }
 }; /* class BitVectorRotateLeftOpTypeRule */
@@ -360,7 +360,7 @@ class BitVectorRotateRightOpTypeRule
                                      TNode n,
                                      bool check)
   {
-    Assert(n.getKind() == kind::BITVECTOR_ROTATE_RIGHT);
+    Assert(n.getKind() == kind::BITVECTOR_ROTATE_RIGHT_OP);
     return nodeManager->builtinOperatorType();
   }
 }; /* class BitVectorRotateRightOpTypeRule */

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index dfd92a8c5c4a1104506d8972d6f2a27e6491a51e..c17e23f055a60e82d7641e6648a85b76558e373e 100644 (file)
--- 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&);