clarify error msg for destructuring assignment

Author: tjhance

source/rust_verify/src/rust_to_vir_expr.rs

@@ -507,7 +507,7 @@ pub(crate) fn pattern_to_vir_unadjusted<'tcx>(
 ) -> Result<vir::ast::Pattern, VirErr> {
     let tcx = bctx.ctxt.tcx;
     let mut pat_typ = typ_of_node(bctx, pat.span, &pat.hir_id, false)?;
-    unsupported_err_unless!(pat.default_binding_modes, pat.span, "complex pattern");
+    unsupported_err_unless!(pat.default_binding_modes, pat.span, "destructuring assignment");
     let pattern = match &pat.kind {
         PatKind::Wild => PatternX::Wildcard(false),
         PatKind::Binding(_binding_mode, canonical, x, subpat) => {

source/rust_verify_test/tests/basic.rs

@@ -641,3 +641,13 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+test_verify_one_file! {
+    #[test] destructuring_assignment_unsupported verus_code! {
+        fn test() {
+            let mut a = 0;
+            let mut b = 0;
+            (a, b) = (1, 2);
+        }
+    } => Err(err) => assert_vir_error_msg(err, "The verifier does not yet support the following Rust feature: destructuring assignment")
+}