From 4fe87e0c8715ee67e5dc9b2cd04ab355fe8b8d64 Mon Sep 17 00:00:00 2001
From: Federico Poli <fpoli@users.noreply.github.com>
Date: Mon, 25 Mar 2024 17:53:59 +0100
Subject: [PATCH] Fix

---
 vir/defs/polymorphic/ast/expr.rs | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

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