Fix

viperproject · Mar 25, 2024 · 4fe87e0 · 4fe87e0
1 parent 9eb4046
commit 4fe87e0
Showing 1 changed file with 1 addition and 4 deletions.
diff --git 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