add regression test, fixes #1334

verus-lang · Jan 17, 2025 · eeca797 · eeca797
1 parent 77551f7
commit eeca797
Showing 1 changed file with 10 additions and 0 deletions.
diff --git 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(())
+}