diff --git a/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs b/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs
index 21384762c370..109227f9097c 100644
--- a/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs
+++ b/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs
@@ -375,8 +375,14 @@ impl<'tcx> GotocCtx<'tcx> {
             "simd_and" => codegen_intrinsic_binop!(bitand),
             "simd_div" => codegen_intrinsic_binop!(div),
             "simd_eq" => codegen_intrinsic_binop!(eq),
+            "simd_extract" => {
+                let vec = fargs.remove(0);
+                let index = fargs.remove(0);
+                self.codegen_expr_to_place(p, vec.index_array(index))
+            }
             "simd_ge" => codegen_intrinsic_binop!(ge),
             "simd_gt" => codegen_intrinsic_binop!(gt),
+            "simd_insert" => self.codegen_intrinsic_simd_insert(fargs, p, cbmc_ret_ty, loc),
             "simd_le" => codegen_intrinsic_binop!(le),
             "simd_lt" => codegen_intrinsic_binop!(lt),
             "simd_mul" => codegen_intrinsic_binop!(mul),
@@ -791,4 +797,33 @@ impl<'tcx> GotocCtx<'tcx> {
             }
         }
     }
+
+    /// Insert is a generic update of a single value in a SIMD vector.
+    /// `P = simd_insert(vector, index, newval)` is here translated to
+    /// `{ T v = vector; v[index] = (cast)newval; P = v; }`
+    ///
+    /// CBMC does not currently seem to implement intrinsics like insert e.g.:
+    /// `**** WARNING: no body for function __builtin_ia32_vec_set_v4si`
+    pub fn codegen_intrinsic_simd_insert(
+        &mut self,
+        mut fargs: Vec<Expr>,
+        p: &Place<'tcx>,
+        cbmc_ret_ty: Type,
+        loc: Location,
+    ) -> Stmt {
+        let vec = fargs.remove(0);
+        let index = fargs.remove(0);
+        let newval = fargs.remove(0);
+        // Type checker should have ensured it's a vector type
+        let elem_ty = cbmc_ret_ty.base_type().unwrap().clone();
+        let tmp = self.gen_temp_variable(cbmc_ret_ty, loc.clone()).to_expr();
+        Stmt::block(
+            vec![
+                Stmt::decl(tmp.clone(), Some(vec), loc.clone()),
+                tmp.clone().index_array(index).assign(newval.cast_to(elem_ty), loc.clone()),
+                self.codegen_expr_to_place(p, tmp),
+            ],
+            loc,
+        )
+    }
 }
diff --git a/src/test/cbmc/SIMD/Construction/main.rs b/src/test/cbmc/SIMD/Construction/main.rs
new file mode 100644
index 000000000000..48d7aa444035
--- /dev/null
+++ b/src/test/cbmc/SIMD/Construction/main.rs
@@ -0,0 +1,39 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#![feature(repr_simd, platform_intrinsics)]
+
+#[repr(simd)]
+#[allow(non_camel_case_types)]
+#[derive(Clone, Copy, PartialEq, Eq)]
+pub struct i64x2(i64, i64);
+
+extern "platform-intrinsic" {
+    fn simd_extract<T, U>(x: T, idx: u32) -> U;
+    fn simd_insert<T, U>(x: T, idx: u32, b: U) -> T;
+}
+
+fn main() {
+    let y = i64x2(0, 1);
+    let z = i64x2(1, 2);
+
+    // Indexing into the vectors
+    assert!(z.0 == 1);
+    assert!(z.1 == 2);
+
+    {
+        // Intrinsic indexing
+        let y_0: i64 = unsafe { simd_extract(y, 0) };
+        let y_1: i64 = unsafe { simd_extract(y, 1) };
+        assert!(y_0 == 0);
+        assert!(y_1 == 1);
+    }
+    {
+        // Intrinsic updating
+        let m = unsafe { simd_insert(y, 0, 1) };
+        let n = unsafe { simd_insert(y, 1, 5) };
+        assert!(m.0 == 1 && m.1 == 1);
+        assert!(n.0 == 0 && n.1 == 5);
+        // Original unchanged
+        assert!(y.0 == 0 && y.1 == 1);
+    }
+}
diff --git a/src/test/cbmc/SIMD/Operators/main.rs b/src/test/cbmc/SIMD/Operators/main.rs
index d9030338f864..c184f2bb32ec 100644
--- a/src/test/cbmc/SIMD/Operators/main.rs
+++ b/src/test/cbmc/SIMD/Operators/main.rs
@@ -41,8 +41,7 @@ fn main() {
         assert_op!(res_mul, simd_mul, y, z, 0, 2);
         assert_op!(res_div, simd_div, v, z, 1, 1);
         assert_op!(res_rem, simd_rem, v, z, 0, 1);
-        assert_op!(res_rem, simd_rem, v, z, 0, 1);
-        assert_op!(res_shr, simd_shl, z, z, 2, 8);
+        assert_op!(res_shl, simd_shl, z, z, 2, 8);
         assert_op!(res_shr, simd_shr, z, y, 1, 1);
         assert_op!(res_and, simd_and, y, v, 0, 1);
         assert_op!(res_or, simd_or, x, y, 0, 1);