From 091724a65f5cdf0855bc5d512b90f1b19210ecd5 Mon Sep 17 00:00:00 2001 From: mayuriphad Date: Wed, 21 Oct 2026 09:58:56 +0530 Subject: [PATCH 1/2] fix(bitvec): return 0 for concrete ADDMOD/MULMOD with a zero modulus Signed-off-by: mayuriphad --- src/halmos/bitvec.py | 6 ++++++ tests/test_bitvec.py | 10 ++++++++++ 2 files changed, 16 insertions(+) diff --git a/src/halmos/bitvec.py b/src/halmos/bitvec.py index e1d6ac3b7..111e0e252 100644 --- a/src/halmos/bitvec.py +++ b/src/halmos/bitvec.py @@ -734,6 +734,9 @@ def addmod( assert size == modulus.size if self.is_concrete and other.is_concrete and modulus.is_concrete: + # mod by zero is zero + if modulus.value == 0: + return HalmosBitVec(0, size=size) return HalmosBitVec((self.value + other.value) % modulus.value, size=size) # to avoid add overflow; and to be a multiple of 8-bit @@ -762,6 +765,9 @@ def mulmod( assert size == modulus.size if self.is_concrete and other.is_concrete and modulus.is_concrete: + # mod by zero is zero + if modulus.value == 0: + return HalmosBitVec(0, size=size) return HalmosBitVec((self.value * other.value) % modulus.value, size=size) # to avoid mul overflow diff --git a/tests/test_bitvec.py b/tests/test_bitvec.py index 1d201f219..f7f0e84e3 100644 --- a/tests/test_bitvec.py +++ b/tests/test_bitvec.py @@ -305,3 +305,13 @@ def test_bool_hashable(): assert y not in dict assert TRUE not in dict assert FALSE in dict + + +@pytest.mark.parametrize("a, b, n, expected", [(2, 3, 0, 0), (2, 3, 4, 1), (7, 5, 1, 0)]) +def test_addmod_concrete(a, b, n, expected): + assert int(BV(a).addmod(BV(b), BV(n))) == expected + + +@pytest.mark.parametrize("a, b, n, expected", [(2, 3, 0, 0), (2, 3, 4, 2), (7, 5, 1, 0)]) +def test_mulmod_concrete(a, b, n, expected): + assert int(BV(a).mulmod(BV(b), BV(n))) == expected From 3a5f1872b8d1c3c6e7df2d10c64cd19887ce47b3 Mon Sep 17 00:00:00 2001 From: mayuriphad Date: Wed, 21 Oct 2026 09:59:06 +0530 Subject: [PATCH 2/2] style: format new bitvec tests Signed-off-by: mayuriphad --- tests/test_bitvec.py | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/tests/test_bitvec.py b/tests/test_bitvec.py index f7f0e84e3..afad21e23 100644 --- a/tests/test_bitvec.py +++ b/tests/test_bitvec.py @@ -307,11 +307,15 @@ def test_bool_hashable(): assert FALSE in dict -@pytest.mark.parametrize("a, b, n, expected", [(2, 3, 0, 0), (2, 3, 4, 1), (7, 5, 1, 0)]) +@pytest.mark.parametrize( + "a, b, n, expected", [(2, 3, 0, 0), (2, 3, 4, 1), (7, 5, 1, 0)] +) def test_addmod_concrete(a, b, n, expected): assert int(BV(a).addmod(BV(b), BV(n))) == expected -@pytest.mark.parametrize("a, b, n, expected", [(2, 3, 0, 0), (2, 3, 4, 2), (7, 5, 1, 0)]) +@pytest.mark.parametrize( + "a, b, n, expected", [(2, 3, 0, 0), (2, 3, 4, 2), (7, 5, 1, 0)] +) def test_mulmod_concrete(a, b, n, expected): assert int(BV(a).mulmod(BV(b), BV(n))) == expected