diff --git a/source/Cargo.lock b/source/Cargo.lock
index b582a9695a..04e38b35f0 100644
--- a/source/Cargo.lock
+++ b/source/Cargo.lock
@@ -795,9 +795,9 @@ dependencies = [
 
 [[package]]
 name = "num-bigint"
-version = "0.4.3"
+version = "0.4.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f93ab6289c7b344a8a9f60f88d80aa20032336fe78da341afc91c8a2341fc75f"
+checksum = "608e7659b5c3d7cba262d894801b9ec9d00de989e8a82bd4bef91d08da45cdc0"
 dependencies = [
  "autocfg",
  "num-integer",
@@ -861,9 +861,9 @@ dependencies = [
 
 [[package]]
 name = "num-traits"
-version = "0.2.15"
+version = "0.2.16"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "578ede34cf02f8924ab9447f50c28075b4d3e5b269972345e7e0372b38c6cdcd"
+checksum = "f30b0abd723be7e2ffca1272140fac1a2f084c77ec3e123c192b66af1ee9e6c2"
 dependencies = [
  "autocfg",
 ]
@@ -1254,7 +1254,7 @@ dependencies = [
  "air",
  "bincode",
  "getopts",
- "num-bigint 0.4.3",
+ "num-bigint 0.4.4",
  "num-format",
  "regex",
  "rust_verify_test_macros",
@@ -1838,7 +1838,7 @@ dependencies = [
  "air",
  "im",
  "indexmap 1.9.3",
- "num-bigint 0.4.3",
+ "num-bigint 0.4.4",
  "num-traits",
  "serde",
  "sha2",
diff --git a/source/rust_verify/Cargo.toml b/source/rust_verify/Cargo.toml
index 1f819a017b..6fc27090dc 100644
--- a/source/rust_verify/Cargo.toml
+++ b/source/rust_verify/Cargo.toml
@@ -12,7 +12,7 @@ serde = "1"
 serde_json = { version = ">=1.0.95", features = ["preserve_order"] }
 bincode = "1.0.1"
 sise = "0.6.0"
-num-bigint = "0.4.3"
+num-bigint = "0.4.4"
 num-format = "0.4.0"
 getopts = { git = "https://github.com/utaal/getopts.git", branch = "parse-partial" }
 regex = "1"
@@ -30,4 +30,4 @@ rust_verify_test_macros = { path = "../rust_verify_test_macros" }
 singular = ["vir/singular", "air/singular"]
 
 [package.metadata.rust-analyzer]
-rustc_private = true
\ No newline at end of file
+rustc_private = true
diff --git a/source/vir/Cargo.toml b/source/vir/Cargo.toml
index 54e0945bee..cafac6994b 100644
--- a/source/vir/Cargo.toml
+++ b/source/vir/Cargo.toml
@@ -10,8 +10,8 @@ edition = "2018"
 air = { path = "../air" }
 vir-macros = { path = "../vir_macros" }
 sise = "0.6.0"
-num-bigint = { version = "0.4.3", features = ["serde"] }
-num-traits= "0.2.15"
+num-bigint = { version = "0.4.4", features = ["serde"] }
+num-traits= "0.2.16"
 im = "15.1.0"
 sha2 = "0.10.2"
 serde = { version = "1", features = ["derive", "rc"] }
diff --git a/source/vir/src/interpreter.rs b/source/vir/src/interpreter.rs
index fe73bf84bd..76cc7071ee 100644
--- a/source/vir/src/interpreter.rs
+++ b/source/vir/src/interpreter.rs
@@ -17,9 +17,9 @@ use air::ast::{Binder, BinderX, Binders, Span};
 use air::messages::{warning, Diagnostics, Message};
 use air::scope_map::ScopeMap;
 use im::Vector;
-use num_bigint::{BigInt, Sign};
+use num_bigint::BigInt;
 use num_traits::identities::Zero;
-use num_traits::{FromPrimitive, One, Signed, ToPrimitive};
+use num_traits::{Euclid, FromPrimitive, One, ToPrimitive};
 use std::collections::HashMap;
 use std::fs::File;
 use std::hash::{Hash, Hasher};
@@ -511,37 +511,6 @@ fn hash_exp<H: Hasher>(state: &mut H, exp: &Exp) {
  * Utility functions  *
  **********************/
 
-// Based on Dafny's C# implementation:
-// https://github.com/dafny-lang/dafny/blob/08744a797296897f4efd486083579e484f57b9dc/Source/DafnyRuntime/DafnyRuntime.cs#L1383
-/// Proper Euclidean division on BigInt
-fn euclidean_div(i1: &BigInt, i2: &BigInt) -> BigInt {
-    // Note: Can be replaced with an inbuilt method on BigInts once
-    // https://github.com/rust-num/num-bigint/pull/245 is merged.
-    use Sign::*;
-    match (i1.sign(), i2.sign()) {
-        (Plus | NoSign, Plus | NoSign) => i1 / i2,
-        (Plus | NoSign, Minus) => -(i1 / (-i2)),
-        (Minus, Plus | NoSign) => -(((-i1) - BigInt::one()) / i2) - BigInt::one(),
-        (Minus, Minus) => (((-i1) - BigInt::one()) / (-i2)) + 1,
-    }
-}
-
-// Based on Dafny's C# implementation:
-// https://github.com/dafny-lang/dafny/blob/08744a797296897f4efd486083579e484f57b9dc/Source/DafnyRuntime/DafnyRuntime.cs#L1436
-/// Proper Euclidean mod on BigInt
-fn euclidean_mod(i1: &BigInt, i2: &BigInt) -> BigInt {
-    // Note: Can be replaced with an inbuilt method on BigInts once
-    // https://github.com/rust-num/num-bigint/pull/245 is merged.
-    use Sign::*;
-    match i1.sign() {
-        Plus | NoSign => i1 % i2.abs(),
-        Minus => {
-            let c = (-i1) % i2.abs();
-            if c.is_zero() { BigInt::zero() } else { i2.abs() - c }
-        }
-    }
-}
-
 /// Truncate a u128 to a fixed width BigInt
 fn u128_to_fixed_width(u: u128, width: u32) -> BigInt {
     match width {
@@ -1221,14 +1190,14 @@ fn eval_expr_internal(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result<Exp, Vi
                                     if i2.is_zero() {
                                         ok_e2(e2) // Treat as symbolic instead of erroring
                                     } else {
-                                        int_new(euclidean_div(i1, i2))
+                                        int_new(i1.div_euclid(i2))
                                     }
                                 }
                                 EuclideanMod => {
                                     if i2.is_zero() {
                                         ok_e2(e2) // Treat as symbolic instead of erroring
                                     } else {
-                                        int_new(euclidean_mod(i1, i2))
+                                        int_new(i1.rem_euclid(i2))
                                     }
                                 }
                             }