From f94e2907144e78d4599eeabfc972f8075030efe3 Mon Sep 17 00:00:00 2001
From: Andrea Lattuada <andrea@lattuada.me>
Date: Tue, 29 Oct 2024 13:46:59 +0100
Subject: [PATCH] allow `#[verifier(external_body)]` again on consts

* add failing test for #1322
---
 source/rust_verify/src/external.rs      |  1 +
 source/rust_verify_test/tests/consts.rs | 15 +++++++++++++++
 2 files changed, 16 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..2ed50a88b 100644
--- a/source/rust_verify_test/tests/consts.rs
+++ b/source/rust_verify_test/tests/consts.rs
@@ -341,3 +341,18 @@ test_verify_one_file! {
         }
     } => Err(err) => assert_one_fails(err)
 }
+
+test_verify_one_file! {
+    #[test] allow_external_body_const_regression_1322_1 verus_code! {
+        #[verifier(external_body)]
+        const A: usize = unimplemented!();
+    } => Ok(())
+}
+
+test_verify_one_file! {
+    // TODO un-ignore once fixed
+    #[ignore] #[test] allow_external_body_const_regression_1322_2 verus_code! {
+        #[verifier(external_body)]
+        const A: usize ensures 32 <= A <= 52 { unimplemented!() }
+    } => Ok(())
+}