From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Sun, 24 Mar 2019 05:58:31 +0000 (-0700)
Subject: BV: Fix typerules for rotate operators. (#2895)
X-Git-Tag: cvc5-1.0.0~4218
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c6e9766a910509583a32e85ad8be55aea550c17c;p=cvc5.git

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 616a03f6b..a9509df42 100644
--- 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 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&);