diff --git a/crates/forge/src/runner.rs b/crates/forge/src/runner.rs
index 591fd65e718c4..dfc9b3f16da07 100644
--- a/crates/forge/src/runner.rs
+++ b/crates/forge/src/runner.rs
@@ -891,22 +891,28 @@ impl<'a, FEN: FoundryEvmNetwork> FunctionRunner<'a, FEN> {
                     &mut raw_call_result,
                     false,
                 );
+                if success {
+                    self.result.symbolic_result(
+                        false,
+                        Some(
+                            "incomplete symbolic execution (Error): symbolic counterexample did not replay"
+                                .to_string(),
+                        ),
+                        None,
+                        stats,
+                    );
+                    self.result.symbolic_portfolio_diagnostics = portfolio_diagnostics;
+                    self.result.symbolic_diagnostics = symbolic_diagnostics;
+                    return self.result;
+                }
+
                 let counterexample = CounterExample::Single(BaseCounterExample::from_fuzz_call(
                     calldata,
                     args,
                     raw_call_result.traces.clone(),
                 ));
                 self.result.extend(raw_call_result);
-                self.result.symbolic_result(
-                    false,
-                    if success {
-                        Some("symbolic counterexample did not replay".to_string())
-                    } else {
-                        reason
-                    },
-                    Some(counterexample),
-                    stats,
-                );
+                self.result.symbolic_result(false, reason, Some(counterexample), stats);
             }
         }
 
@@ -1028,13 +1034,27 @@ impl<'a, FEN: FoundryEvmNetwork> FunctionRunner<'a, FEN> {
             SymbolicInvariantRunResult::Counterexample { sequence, stats } => {
                 let (replayed, reason, replay_sequence) =
                     self.replay_symbolic_invariant_sequence(func, &sequence, fail_on_revert);
+                if !replayed {
+                    let reason = reason.map_or_else(
+                        || "symbolic invariant counterexample did not replay".to_string(),
+                        |reason| {
+                            format!("symbolic invariant counterexample did not replay: {reason}")
+                        },
+                    );
+                    self.result.symbolic_result(
+                        false,
+                        Some(format!("incomplete symbolic invariant execution (Error): {reason}")),
+                        None,
+                        stats,
+                    );
+                    self.result.symbolic_portfolio_diagnostics = portfolio_diagnostics;
+                    self.result.symbolic_diagnostics = symbolic_diagnostics;
+                    return self.result;
+                }
+
                 self.result.symbolic_result(
                     false,
-                    if replayed {
-                        reason.or_else(|| Some("symbolic invariant counterexample".to_string()))
-                    } else {
-                        Some("symbolic invariant counterexample did not replay".to_string())
-                    },
+                    reason.or_else(|| Some("symbolic invariant counterexample".to_string())),
                     Some(CounterExample::Sequence(replay_sequence.len(), replay_sequence)),
                     stats,
                 );
diff --git a/crates/forge/tests/cli/test_cmd/symbolic_storage.rs b/crates/forge/tests/cli/test_cmd/symbolic_storage.rs
index becd899044527..3c8973c121174 100644
--- a/crates/forge/tests/cli/test_cmd/symbolic_storage.rs
+++ b/crates/forge/tests/cli/test_cmd/symbolic_storage.rs
@@ -2,7 +2,7 @@ use super::symbolic_helpers::assert_relevant_lines;
 use foundry_common::sh_eprintln;
 use foundry_test_utils::{forgetest_init, str, util::OutputExt};
 
-use super::symbolic_helpers::{assert_symbolic, assert_symbolic_witness, z3_available};
+use super::symbolic_helpers::{assert_symbolic, z3_available};
 use crate::skip_unless_z3;
 
 forgetest_init!(symbolic_mapping_storage_finds_counterexample, |prj, cmd| {
@@ -437,8 +437,10 @@ checkSvmArbitraryStorage(address)
 
 // Reading an unwritten mapping at a symbolic key must yield a fresh symbolic
 // value, not a concrete zero. The assertion below claims that no caller is an
-// admin; because nothing has ever written to `isAdmin`, the solver must still
-// be able to satisfy `isAdmin[user] == true` and produce a counterexample.
+// admin; because nothing has ever written to `isAdmin`, the solver can satisfy
+// `isAdmin[user] == true`. That candidate does not replay concretely from the
+// default concrete storage value, so Forge must report Incomplete instead of a
+// user-facing counterexample.
 forgetest_init!(symbolic_sload_unwritten_mapping_default_layout, |prj, cmd| {
     skip_unless_z3!("symbolic_sload_unwritten_mapping_default_layout");
 
@@ -455,7 +457,7 @@ contract SymbolicSLoadUnwrittenMapping {
 "#,
     );
 
-    assert_symbolic_witness(cmd.args([
+    assert_symbolic(cmd.args([
         "test",
         "--symbolic",
         "--match-test",
@@ -466,7 +468,7 @@ contract SymbolicSLoadUnwrittenMapping {
 ...
 Failing tests:
 Encountered 1 failing test in test/SymbolicSLoadUnwrittenMapping.t.sol:SymbolicSLoadUnwrittenMapping
-[FAIL: symbolic counterexample did not replay; counterexample: [CALLDATA] [ARGS]] checkNoUserIsAdmin(address) ([METRICS])
+[FAIL: incomplete symbolic execution (Error): symbolic counterexample did not replay] checkNoUserIsAdmin(address) ([METRICS])
 
 Encountered a total of 1 failing tests, 0 tests succeeded