diff --git a/src/halmos/bitvec.py b/src/halmos/bitvec.py
index e1d6ac3b..8b2559b7 100644
--- a/src/halmos/bitvec.py
+++ b/src/halmos/bitvec.py
@@ -734,6 +734,8 @@ def addmod(
         assert size == modulus.size
 
         if self.is_concrete and other.is_concrete and modulus.is_concrete:
+            if modulus.value == 0:
+                return modulus
             return HalmosBitVec((self.value + other.value) % modulus.value, size=size)
 
         # to avoid add overflow; and to be a multiple of 8-bit
@@ -762,6 +764,8 @@ def mulmod(
         assert size == modulus.size
 
         if self.is_concrete and other.is_concrete and modulus.is_concrete:
+            if modulus.value == 0:
+                return modulus
             return HalmosBitVec((self.value * other.value) % modulus.value, size=size)
 
         # to avoid mul overflow
diff --git a/tests/test_sevm.py b/tests/test_sevm.py
index ef05c2af..0d03c5de 100644
--- a/tests/test_sevm.py
+++ b/tests/test_sevm.py
@@ -192,6 +192,7 @@ def byte_of(i, x):
         (o(EVM.SMOD), [x, BV(0)], BV(0)),
         (o(EVM.SMOD), [x, BV(1)], BV(0)),
         (o(EVM.ADDMOD), [BV(4), BV(1), BV(3)], BV(2)),
+        (o(EVM.ADDMOD), [BV(4), BV(1), BV(0)], BV(0)),
         (o(EVM.ADDMOD), [x, y, BV(0)], BV(0)),
         (o(EVM.ADDMOD), [x, y, BV(1)], BV(0)),
         (
@@ -229,6 +230,7 @@ def byte_of(i, x):
             BV(1),
         ),
         (o(EVM.MULMOD), [BV(5), BV(1), BV(3)], BV(2)),
+        (o(EVM.MULMOD), [BV(5), BV(1), BV(0)], BV(0)),
         (o(EVM.MULMOD), [x, y, BV(0)], BV(0)),
         (o(EVM.MULMOD), [x, y, BV(1)], BV(0)),
         (