Fix

viperproject · Mar 25, 2024 · 0607b5f · 0607b5f
1 parent 4fe87e0
commit 0607b5f
Showing 1 changed file with 1 addition and 4 deletions.
diff --git a/vir/src/legacy/ast/expr.rs b/vir/src/legacy/ast/expr.rs
@@ -575,10 +575,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