diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp index 6f9c173c2f2..f16571b8d7a 100644 --- a/src/theory/bv/int_blaster.cpp +++ b/src/theory/bv/int_blaster.cpp @@ -478,7 +478,7 @@ Node IntBlaster::translateWithChildren( } case Kind::BITVECTOR_BITOF: { - // ((_ extract i j) a) is a / 2^j mod 2^{i-j+1} + // ((_ bitof i) a) is a / 2^i mod 2 // original = a[i:j] uint32_t i = original.getOperator().getConst().d_bitIndex; Assert(i >= 0);