From eeca797f7645e2c90065870bcd86267d40d66284 Mon Sep 17 00:00:00 2001
From: Andrea Lattuada <andrea@mpi-sws.org>
Date: Fri, 17 Jan 2025 21:04:56 +0100
Subject: [PATCH] add regression test, fixes #1334

---
 source/rust_verify_test/tests/regression.rs | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/source/rust_verify_test/tests/regression.rs b/source/rust_verify_test/tests/regression.rs
index b45a3804b..a12218326 100644
--- a/source/rust_verify_test/tests/regression.rs
+++ b/source/rust_verify_test/tests/regression.rs
@@ -1328,3 +1328,13 @@ test_verify_one_file! {
         }
     } => Err(e) => assert_vir_error_msg(e, "use the universal function call syntax to disambiguate")
 }
+
+test_verify_one_file_with_options! {
+    #[test] const_in_array_types_regression_1334 ["vstd"] => verus_code! {
+        const TEST: usize = 4;
+
+        pub fn get_array() -> [u8; TEST] {
+            return [0; TEST]
+        }
+    } => Ok(())
+}