diff options
Diffstat (limited to 'src/theory/bv/kinds')
| -rw-r--r-- | src/theory/bv/kinds | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index da2833ca0..66ee02c63 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -79,8 +79,8 @@ operator BITVECTOR_REDOR 1 "bit-vector redor" operator BITVECTOR_REDAND 1 "bit-vector redand" operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bit-blasting (internal-only symbol)" -operator BITVECTOR_ACKERMANIZE_UDIV 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal-only symbol)" -operator BITVECTOR_ACKERMANIZE_UREM 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal-only symbol)" +operator BITVECTOR_ACKERMANNIZE_UDIV 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal-only symbol)" +operator BITVECTOR_ACKERMANNIZE_UREM 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal-only symbol)" constant BITVECTOR_BITOF_OP \ ::CVC4::BitVectorBitOf \ @@ -187,8 +187,8 @@ typerule BITVECTOR_REDAND ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule typerule BITVECTOR_EAGER_ATOM ::CVC4::theory::bv::BitVectorEagerAtomTypeRule -typerule BITVECTOR_ACKERMANIZE_UDIV ::CVC4::theory::bv::BitVectorAckermanizationUdivTypeRule -typerule BITVECTOR_ACKERMANIZE_UREM ::CVC4::theory::bv::BitVectorAckermanizationUremTypeRule +typerule BITVECTOR_ACKERMANNIZE_UDIV ::CVC4::theory::bv::BitVectorAckermanizationUdivTypeRule +typerule BITVECTOR_ACKERMANNIZE_UREM ::CVC4::theory::bv::BitVectorAckermanizationUremTypeRule typerule BITVECTOR_EXTRACT_OP ::CVC4::theory::bv::BitVectorExtractOpTypeRule typerule BITVECTOR_EXTRACT ::CVC4::theory::bv::BitVectorExtractTypeRule |