From 8fa4069ca5ab7eb056fb58057b1e6bb0f034c195 Mon Sep 17 00:00:00 2001
From: Andrea Lattuada <andrea@lattuada.me>
Date: Tue, 29 Oct 2024 13:46:59 +0100
Subject: [PATCH] write test for regression introduced by bf90ae0d and reported
 by #1322, partial fix

---
 source/rust_verify/src/external.rs      | 1 +
 source/rust_verify_test/tests/consts.rs | 7 +++++++
 2 files changed, 8 insertions(+)

diff --git a/source/rust_verify/src/external.rs b/source/rust_verify/src/external.rs
index 95ccb5d91..7e23d834e 100644
--- a/source/rust_verify/src/external.rs
+++ b/source/rust_verify/src/external.rs
@@ -478,6 +478,7 @@ impl<'a> GeneralItem<'a> {
                 ItemKind::Struct(..) => true,
                 ItemKind::Enum(..) => true,
                 ItemKind::Union(..) => true,
+                ItemKind::Const(..) => true,
                 _ => false,
             },
             GeneralItem::ForeignItem(_) => false,
diff --git a/source/rust_verify_test/tests/consts.rs b/source/rust_verify_test/tests/consts.rs
index 2bb6cdb9e..a38973dc3 100644
--- a/source/rust_verify_test/tests/consts.rs
+++ b/source/rust_verify_test/tests/consts.rs
@@ -341,3 +341,10 @@ test_verify_one_file! {
         }
     } => Err(err) => assert_one_fails(err)
 }
+
+test_verify_one_file! {
+    #[test] allow_external_body_const verus_code! {
+        #[verifier(external_body)]
+        const A: usize ensures 32 <= A <= 52 { unimplemented!() }
+    } => Ok(())
+}