diff --git a/compiler/noirc_evaluator/src/ssa/mod.rs b/compiler/noirc_evaluator/src/ssa/mod.rs
index 198ca56c8b0..7a3baee699d 100644
--- a/compiler/noirc_evaluator/src/ssa/mod.rs
+++ b/compiler/noirc_evaluator/src/ssa/mod.rs
@@ -192,7 +192,13 @@ pub fn primary_passes(options: &SsaEvaluatorOptions) -> Vec<SsaPass> {
         SsaPass::new_try(
             Ssa::verify_no_dynamic_indices_to_references,
             "Verifying no dynamic array indices to reference value elements",
-        ),
+        )
+        .and_then(|ssa| {
+            // Deferred sanity checks that don't modify the SSA, just panic if we have something unexpected
+            // that we don't know how to attribute to a concrete error with the Noir code.
+            ssa.dead_instruction_elimination_post_check(true);
+            ssa
+        }),
     ]
 }
 
diff --git a/compiler/noirc_evaluator/src/ssa/opt/die.rs b/compiler/noirc_evaluator/src/ssa/opt/die.rs
index 3870bed22f7..82cd85ef03d 100644
--- a/compiler/noirc_evaluator/src/ssa/opt/die.rs
+++ b/compiler/noirc_evaluator/src/ssa/opt/die.rs
@@ -54,14 +54,6 @@ impl Ssa {
         flattened: bool,
         skip_brillig: bool,
     ) -> Ssa {
-        // Perform post-checks on the SSA.
-        let check = |ssa: Ssa| {
-            // Check that we have established the properties expected from this pass.
-            #[cfg(debug_assertions)]
-            ssa.functions.values().for_each(|f| die_post_check(f, flattened));
-            ssa
-        };
-
         let mut previous_unused_params = None;
         loop {
             let (new_ssa, result) =
@@ -75,13 +67,13 @@ impl Ssa {
 
             // If there are no unused parameters, return early
             if !has_unused {
-                return check(new_ssa);
+                return new_ssa;
             }
 
             if let Some(previous) = &previous_unused_params {
                 // If no changes to dead parameters occurred, return early
                 if previous == &result.unused_parameters {
-                    return check(new_ssa);
+                    return new_ssa;
                 }
             }
 
@@ -114,6 +106,19 @@ impl Ssa {
 
         (self, result)
     }
+
+    /// Sanity check on the final SSA, panicking if the assumptions don't hold.
+    ///
+    /// Done as a separate step so that we can put it after other passes which provide
+    /// concrete feedback about where the problem with the Noir code might be, such as
+    /// dynamic indexing of arrays with references in ACIR. We can look up the callstack
+    /// of the offending instruction here as well, it's just not clear what error message
+    /// to return, besides the fact that mem2reg was unable to eliminate something.
+    #[cfg_attr(not(debug_assertions), allow(unused_variables))]
+    pub(crate) fn dead_instruction_elimination_post_check(&self, flattened: bool) {
+        #[cfg(debug_assertions)]
+        self.functions.values().for_each(|f| die_post_check(f, flattened));
+    }
 }
 
 impl Function {
diff --git a/tooling/ast_fuzzer/src/program/func.rs b/tooling/ast_fuzzer/src/program/func.rs
index f0de45e1435..51b598b4b8c 100644
--- a/tooling/ast_fuzzer/src/program/func.rs
+++ b/tooling/ast_fuzzer/src/program/func.rs
@@ -220,6 +220,9 @@ pub(super) struct FunctionContext<'a> {
     in_loop: bool,
     /// Indicator of computing an expression that should not contain dynamic input.
     in_no_dynamic: bool,
+    /// Indicator of being affected by dynamic input, in which case we should refrain
+    /// from using expression that requires no-dynamic mode.
+    in_dynamic: bool,
     /// All the functions callable from this one, with the types we can
     /// produce from their return value.
     call_targets: BTreeMap<CallableId, HashSet<Type>>,
@@ -285,6 +288,7 @@ impl<'a> FunctionContext<'a> {
             dynamics,
             in_loop: false,
             in_no_dynamic: false,
+            in_dynamic: false,
             call_targets,
             next_ident_id: 0,
             has_call: false,
@@ -361,6 +365,16 @@ impl<'a> FunctionContext<'a> {
         self.dynamics.contains(id)
     }
 
+    /// Check if a source type can be used inside a dynamic input context to produce some target type.
+    fn can_be_used_in_dynamic(&self, src_type: &Type, tgt_type: &Type) -> bool {
+        // Dynamic inputs are restricted only in ACIR
+        self.unconstrained()
+        // If we are looking for the exact type, it's okay.
+            || src_type == tgt_type
+            // But we can't index an array with references.
+            || !(types::is_array_or_slice(src_type) && types::contains_reference(src_type) )
+    }
+
     /// Choose a producer for a type, preferring local variables over global ones.
     fn choose_producer(
         &self,
@@ -369,10 +383,15 @@ impl<'a> FunctionContext<'a> {
     ) -> arbitrary::Result<Option<VariableId>> {
         // Check if we have something that produces this exact type.
         if u.ratio(7, 10)? {
-            let producer = if self.in_no_dynamic {
-                self.locals
-                    .current()
-                    .choose_producer_filtered(u, typ, |id, _| !self.is_dynamic(id))?
+            let producer = if self.in_no_dynamic || self.in_dynamic {
+                self.locals.current().choose_producer_filtered(
+                    u,
+                    typ,
+                    |id, (_, _, producer_type)| {
+                        (!self.in_no_dynamic || !self.is_dynamic(id))
+                            && (!self.in_dynamic || self.can_be_used_in_dynamic(producer_type, typ))
+                    },
+                )?
             } else {
                 self.locals.current().choose_producer(u, typ)?
             };
@@ -389,10 +408,13 @@ impl<'a> FunctionContext<'a> {
             return self
                 .locals
                 .current()
-                .choose_producer_filtered(u, typ.as_ref(), |id, (mutable, _, prod)| {
+                .choose_producer_filtered(u, typ.as_ref(), |id, (mutable, _, producer_type)| {
                     *mutable
-                        && (typ.as_ref() == prod || !types::is_array_or_slice(prod))
+                        && (typ.as_ref() == producer_type
+                            || !types::is_array_or_slice(producer_type))
                         && (!self.in_no_dynamic || !self.is_dynamic(id))
+                        && (!self.in_dynamic
+                            || self.can_be_used_in_dynamic(producer_type, typ.as_ref()))
                 })
                 .map(|id| id.map(VariableId::Local));
         }
@@ -598,7 +620,12 @@ impl<'a> FunctionContext<'a> {
             return Ok(Some((src_expr, src_dyn)));
         }
 
-        // Mutable references to array elements are currently unsupported
+        // Some types cannot be accessed in certain contexts.
+        if self.in_dynamic && !self.can_be_used_in_dynamic(src_type, tgt_type) {
+            return Ok(None);
+        }
+
+        // Mutable references to array elements are currently unsupported.
         if types::is_array_or_slice(src_type) {
             src_mutable = false;
         }
@@ -1226,6 +1253,12 @@ impl<'a> FunctionContext<'a> {
 
         let (cond, cond_dyn) = self.gen_expr(u, &Type::Bool, max_depth, Flags::CONDITION)?;
 
+        // If the `if` condition uses dynamic input, we cannot access certain constructs in the body in ACIR.
+        // Note that this would be the case for `while` and `for` as well, however `while` is not used in ACIR,
+        // and `for` has its own restriction of having to have compile-time boundaries, so this is only done where necessary.
+        let in_dynamic = self.in_dynamic || cond_dyn;
+        let was_in_dynamic = std::mem::replace(&mut self.in_dynamic, in_dynamic);
+
         let (cons, cons_dyn) = {
             if flags.allow_blocks {
                 self.gen_block(u, typ)?
@@ -1246,6 +1279,7 @@ impl<'a> FunctionContext<'a> {
             Some(expr)
         };
 
+        self.in_dynamic = was_in_dynamic;
         let alt_dyn = alt.as_ref().is_some_and(|(_, d)| *d);
         let is_dyn = cond_dyn || cons_dyn || alt_dyn;