diff --git a/src/komet/kdist/soroban-semantics/data.md b/src/komet/kdist/soroban-semantics/data.md
index 842d0bf..0b830f6 100644
--- a/src/komet/kdist/soroban-semantics/data.md
+++ b/src/komet/kdist/soroban-semantics/data.md
@@ -179,6 +179,8 @@ module HOST-OBJECT
     rule getTagWithFlag(true, I64(_))    => 65
     rule getTagWithFlag(true, U128(_))   => 68
     rule getTagWithFlag(true, I128(_))   => 69
+    rule getTagWithFlag(true, U256(_))   => 70
+    rule getTagWithFlag(true, I256(_))   => 71
     rule getTagWithFlag(true, Symbol(_)) => 74
     rule getTagWithFlag(_,    SCV)       => getTag(SCV)      [owise]
    
diff --git a/src/komet/kdist/soroban-semantics/host/integer.md b/src/komet/kdist/soroban-semantics/host/integer.md
index aca8f0e..d09397e 100644
--- a/src/komet/kdist/soroban-semantics/host/integer.md
+++ b/src/komet/kdist/soroban-semantics/host/integer.md
@@ -351,7 +351,7 @@ negative value is converted to its unsigned form before shifting.
 
 The i256 arithmetic host functions are *checked*: the result must be
 representable, and the divisor must be non-zero. Otherwise the host fails the
-call with `(ErrValue, ArithDomain)` rather than wrapping around.
+call with `(ErrObject, ArithDomain)` rather than wrapping around.
 
 The first Wasm argument is on top of the host stack (`loadArgs` pushes the
 arguments in reverse), so `A` is the left-hand side.
@@ -367,7 +367,7 @@ arguments in reverse), so `A` is the left-hand side.
       requires inRangeInt(i256, Signed, A +Int B)
 
     rule [hostCallAux-i256-add-overflow]:
-        <instrs> hostCallAux ( "i" , "v" ) => #throw(ErrValue, ArithDomain) ... </instrs>
+        <instrs> hostCallAux ( "i" , "v" ) => #throw(ErrObject, ArithDomain) ... </instrs>
         <hostStack> I256(A) : I256(B) : S => S </hostStack>
       requires notBool inRangeInt(i256, Signed, A +Int B)
 ```
@@ -385,7 +385,7 @@ arguments in reverse), so `A` is the left-hand side.
       requires inRangeInt(i256, Signed, A -Int B)
 
     rule [hostCallAux-i256-sub-overflow]:
-        <instrs> hostCallAux ( "i" , "w" ) => #throw(ErrValue, ArithDomain) ... </instrs>
+        <instrs> hostCallAux ( "i" , "w" ) => #throw(ErrObject, ArithDomain) ... </instrs>
         <hostStack> I256(A) : I256(B) : S => S </hostStack>
       requires notBool inRangeInt(i256, Signed, A -Int B)
 ```
@@ -403,7 +403,7 @@ arguments in reverse), so `A` is the left-hand side.
       requires inRangeInt(i256, Signed, A *Int B)
 
     rule [hostCallAux-i256-mul-overflow]:
-        <instrs> hostCallAux ( "i" , "x" ) => #throw(ErrValue, ArithDomain) ... </instrs>
+        <instrs> hostCallAux ( "i" , "x" ) => #throw(ErrObject, ArithDomain) ... </instrs>
         <hostStack> I256(A) : I256(B) : S => S </hostStack>
       requires notBool inRangeInt(i256, Signed, A *Int B)
 ```
@@ -427,12 +427,12 @@ rather than range-checking `A /Int B`, so no side condition divides.
       [preserves-definedness] // 'A /Int B' is defined for non-zero B
 
     rule [hostCallAux-i256-div-by-zero]:
-        <instrs> hostCallAux ( "i" , "y" ) => #throw(ErrValue, ArithDomain) ... </instrs>
+        <instrs> hostCallAux ( "i" , "y" ) => #throw(ErrObject, ArithDomain) ... </instrs>
         <hostStack> I256(_A) : I256(B) : S => S </hostStack>
       requires B ==Int 0
 
     rule [hostCallAux-i256-div-overflow]:
-        <instrs> hostCallAux ( "i" , "y" ) => #throw(ErrValue, ArithDomain) ... </instrs>
+        <instrs> hostCallAux ( "i" , "y" ) => #throw(ErrObject, ArithDomain) ... </instrs>
         <hostStack> I256(A) : I256(B) : S => S </hostStack>
       requires A ==Int minInt(i256, Signed) andBool B ==Int -1
 ```
@@ -440,9 +440,9 @@ rather than range-checking `A /Int B`, so no side condition divides.
 ## i256_rem_euclid
 
 Euclidean modulo: the result is always non-negative, whatever the signs of the
-operands. K's `modInt` takes the sign of its divisor, so dividing by `absInt(B)`
-gives exactly Rust's `rem_euclid`. The quotient never leaves the range, so a
-zero divisor is the only failure.
+operands. K's `modInt` is e-division, so it already lands in `[0, absInt(B))`
+and agrees with Rust's `rem_euclid`. `checked_rem_euclid` rejects the same two
+operand pairs as `checked_div`: a zero divisor, and `i256::MIN` by `-1`.
 
 ```k
     rule [hostCallAux-i256-rem-euclid]:
@@ -453,12 +453,14 @@ zero divisor is the only failure.
         </instrs>
         <hostStack> I256(A) : I256(B) : S => S </hostStack>
       requires B =/=Int 0
+       andBool notBool (A ==Int minInt(i256, Signed) andBool B ==Int -1)
       [preserves-definedness] // 'A modInt absInt(B)' is defined for non-zero B
 
     rule [hostCallAux-i256-rem-euclid-error]:
-        <instrs> hostCallAux ( "i" , "z" ) => #throw(ErrValue, ArithDomain) ... </instrs>
-        <hostStack> I256(_A) : I256(B) : S => S </hostStack>
+        <instrs> hostCallAux ( "i" , "z" ) => #throw(ErrObject, ArithDomain) ... </instrs>
+        <hostStack> I256(A) : I256(B) : S => S </hostStack>
       requires B ==Int 0
+        orBool (A ==Int minInt(i256, Signed) andBool B ==Int -1)
 ```
 
 ```k
diff --git a/src/tests/integration/data/i256.wast b/src/tests/integration/data/i256.wast
index c51108d..10806a5 100644
--- a/src/tests/integration/data/i256.wast
+++ b/src/tests/integration/data/i256.wast
@@ -268,7 +268,7 @@ callTx(
   Contract(b"test-sc"),
   "add",
   ListItem(I256(2 ^Int 255 -Int 1)) ListItem(I256(1)),
-  Error(ErrValue, ArithDomain)
+  Error(ErrObject, ArithDomain)
 )
 
 callTx(
@@ -292,7 +292,7 @@ callTx(
   Contract(b"test-sc"),
   "sub",
   ListItem(I256(0 -Int 2 ^Int 255)) ListItem(I256(1)),
-  Error(ErrValue, ArithDomain)
+  Error(ErrObject, ArithDomain)
 )
 
 callTx(
@@ -317,7 +317,7 @@ callTx(
   Contract(b"test-sc"),
   "mul",
   ListItem(I256(2 ^Int 200)) ListItem(I256(2 ^Int 200)),
-  Error(ErrValue, ArithDomain)
+  Error(ErrObject, ArithDomain)
 )
 
 ;; Division truncates toward zero.
@@ -358,7 +358,7 @@ callTx(
   Contract(b"test-sc"),
   "div",
   ListItem(I256(1)) ListItem(I256(0)),
-  Error(ErrValue, ArithDomain)
+  Error(ErrObject, ArithDomain)
 )
 
 ;; i256::MIN / -1 is the one division that overflows.
@@ -367,7 +367,7 @@ callTx(
   Contract(b"test-sc"),
   "div",
   ListItem(I256(0 -Int 2 ^Int 255)) ListItem(I256(0 -Int 1)),
-  Error(ErrValue, ArithDomain)
+  Error(ErrObject, ArithDomain)
 )
 
 ;; Euclidean modulo is never negative, whatever the signs of the operands.
@@ -408,7 +408,17 @@ callTx(
   Contract(b"test-sc"),
   "rem",
   ListItem(I256(1)) ListItem(I256(0)),
-  Error(ErrValue, ArithDomain)
+  Error(ErrObject, ArithDomain)
+)
+
+;; `checked_rem_euclid` rejects i256::MIN % -1 as well, even though the
+;; mathematical remainder (0) is representable.
+callTx(
+  Account(b"test-caller"),
+  Contract(b"test-sc"),
+  "rem",
+  ListItem(I256(0 -Int 2 ^Int 255)) ListItem(I256(0 -Int 1)),
+  Error(ErrObject, ArithDomain)
 )
 
 setExitCode(0)