diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs
index 4595a244a..b1b2ee710 100644
--- a/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs
+++ b/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs
@@ -1942,6 +1942,8 @@ callFunction defSet instr tailCall_ fnTy fn args assign_f
                  , "llvm.dbg.declare"
                  , "llvm.dbg.addr"
                  , "llvm.dbg.value"
+                 , "llvm.dbg.assign" -- Added in LLVM 16
+                 , "llvm.experimental.noalias.scope.decl" -- Added in LLVM 12
                  , "llvm.lifetime.start"
                  , "llvm.lifetime.start.p0"
                  , "llvm.lifetime.start.p0i8"
diff --git a/crux-llvm/test-data/golden/T1196.c b/crux-llvm/test-data/golden/T1196.c
new file mode 100644
index 000000000..9ab75504f
--- /dev/null
+++ b/crux-llvm/test-data/golden/T1196.c
@@ -0,0 +1,14 @@
+void foo(int* restrict p0, int* restrict p1) {
+	*p0 = *p1;
+}
+
+__attribute__((noinline)) void test_inline_foo(int* p0, int* p1) {
+	foo(p0, p1);
+}
+
+int main(void) {
+    int p0 = 0;
+    int p1 = 1;
+    test_inline_foo(&p0, &p1);
+    return 0;
+}
diff --git a/crux-llvm/test-data/golden/T1196.z3.good b/crux-llvm/test-data/golden/T1196.z3.good
new file mode 100644
index 000000000..9c7ea10d9
--- /dev/null
+++ b/crux-llvm/test-data/golden/T1196.z3.good
@@ -0,0 +1 @@
+[Crux] Overall status: Valid.
diff --git a/crux-llvm/test-data/golden/T1204.c b/crux-llvm/test-data/golden/T1204.c
new file mode 100644
index 000000000..ea757c3ab
--- /dev/null
+++ b/crux-llvm/test-data/golden/T1204.c
@@ -0,0 +1,8 @@
+__attribute__((noinline)) int foo(int x[2]) {
+  return x[0];
+}
+
+int main(void) {
+  int x[2] = { 0, 0 };
+  return foo(x);
+}
diff --git a/crux-llvm/test-data/golden/T1204.z3.good b/crux-llvm/test-data/golden/T1204.z3.good
new file mode 100644
index 000000000..9c7ea10d9
--- /dev/null
+++ b/crux-llvm/test-data/golden/T1204.z3.good
@@ -0,0 +1 @@
+[Crux] Overall status: Valid.