diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index e3ce64f753..024abbbdf2 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -163,8 +163,8 @@ private def synthesizeUsingDefault : TermElabM Bool := do
 
 /-- Report an error for each synthetic metavariable that could not be resolved. -/
 private def reportStuckSyntheticMVars : TermElabM Unit := do
-  let s ← get
-  for mvarSyntheticDecl in s.syntheticMVars do
+  let syntheticMVars ← modifyGet fun s => (s.syntheticMVars, { s with syntheticMVars := [] })
+  for mvarSyntheticDecl in syntheticMVars do
     withRef mvarSyntheticDecl.stx do
     match mvarSyntheticDecl.kind with
     | SyntheticMVarKind.typeClass =>
diff --git a/tests/lean/297.lean.expected.out b/tests/lean/297.lean.expected.out
index df5b44d533..59b45f8d44 100644
--- a/tests/lean/297.lean.expected.out
+++ b/tests/lean/297.lean.expected.out
@@ -1,6 +1,4 @@
 297.lean:1:10-1:11: error: typeclass instance problem is stuck, it is often due to metavariables
   OfNat (Sort ?u) 0
 297.lean:1:13-3:1: error: invalid universe level, u_1 is not greater than 0
-297.lean:1:10-1:11: error: failed to synthesize instance
-  OfNat (Sort u_1) 0
 297.lean:1:8-1:9: error: (kernel) declaration has metavariables 'r'