diff --git a/vir/defs/polymorphic/ast/expr.rs b/vir/defs/polymorphic/ast/expr.rs
index fbf928b3588..f5393c586be 100644
--- a/vir/defs/polymorphic/ast/expr.rs
+++ b/vir/defs/polymorphic/ast/expr.rs
@@ -319,10 +319,7 @@ impl Expr {
     /// Encode Rust's division. This is *not* Viper's division.
     pub fn div(left: Expr, right: Expr) -> Self {
         Expr::ite(
-            Expr::or(
-                Expr::ge_cmp(left.clone(), 0.into()),
-                Expr::eq_cmp(Expr::modulo(left.clone(), right.clone()), 0.into()),
-            ),
+            Expr::ge_cmp(left.clone(), 0.into()),
             // positive value or left % right == 0
             Expr::unsigned_div(left.clone(), right.clone()),
             // negative value