From c3813c8876a53ecc568dacf1dca4c3417dd243cb Mon Sep 17 00:00:00 2001
From: Jay Lorch <jaylorch@gmail.com>
Date: Tue, 3 Mar 2026 15:16:35 -0800
Subject: [PATCH] Avoid some build errors

---
 Cargo.toml            | 3 +++
 src/builtins/utils.rs | 2 --
 src/number.rs         | 5 ++++-
 3 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/Cargo.toml b/Cargo.toml
index 57f0b52..b576fad 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -208,3 +208,6 @@ doctest=false
 # RUSTDOCFLAGS="--cfg docsrs" cargo +nightly doc --all-features --no-deps
 all-features = true
 rustdoc-args = ["--cfg", "docsrs"]
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(verus_keep_ghost)'] }
diff --git a/src/builtins/utils.rs b/src/builtins/utils.rs
index 51ef866..65de2c9 100644
--- a/src/builtins/utils.rs
+++ b/src/builtins/utils.rs
@@ -13,8 +13,6 @@ use alloc::collections::{BTreeMap, BTreeSet};
 
 use anyhow::{bail, Result};
 
-use vstd::prelude::*;
-
 #[inline]
 pub fn enforce_limit() -> Result<()> {
     crate::utils::limits::check_memory_limit_if_needed().map_err(anyhow::Error::new)
diff --git a/src/number.rs b/src/number.rs
index d5ae5b7..90ac56f 100644
--- a/src/number.rs
+++ b/src/number.rs
@@ -28,14 +28,17 @@ use serde::ser::Serializer;
 use serde::Serialize;
 
 use vstd::prelude::*;
+#[cfg(verus_keep_ghost)]
 use vstd::float::*;
+#[cfg(verus_keep_ghost)]
 use vstd::std_specs::convert::*;
+#[cfg(verus_keep_ghost)]
 use vstd::std_specs::cmp::*;
 
 use crate::*;
+
 use crate::verusspec::bigint::*;
 use crate::verusspec::float::*;
-use crate::verusspec::utils::*;
 
 verus! {