From 8405689bf8ae8a918015b51d740ebe653753860a Mon Sep 17 00:00:00 2001 From: Yoni Zohar Date: Wed, 22 Nov 2023 13:48:13 +0200 Subject: [PATCH] comment --- src/theory/bv/int_blaster.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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);