diff --git a/source/rust_verify_test/tests/consts.rs b/source/rust_verify_test/tests/consts.rs index 4bb558fae..92647199c 100644 --- a/source/rust_verify_test/tests/consts.rs +++ b/source/rust_verify_test/tests/consts.rs @@ -406,3 +406,10 @@ test_verify_one_file! { } } => Ok(()) } + +test_verify_one_file! { + #[test] allow_external_body_const_regression_1322 verus_code! { + #[verifier(external_body)] + const A: usize = unimplemented!(); + } => Err(err) => assert_rust_error_msg(err, "evaluation of constant value failed") +}