diff --git a/src/halmos/bitvec.py b/src/halmos/bitvec.py
index e1d6ac3b..111e0e25 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 1d201f21..afad21e2 100644
--- a/tests/test_bitvec.py
+++ b/tests/test_bitvec.py
@@ -305,3 +305,17 @@ 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