diff --git a/verification/check.sh b/verification/check.sh
index 4ad0d8a..89e80d9 100755
--- a/verification/check.sh
+++ b/verification/check.sh
@@ -194,7 +194,7 @@ lake env bash -c "
   } > \"\$AUD\"
   OUT=\$(LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1)
   echo \"\$OUT\"
-  rm -f \"\$AUD\"
+  rm -f \"\$AUD\" \"\${AUD%.lean}.olean\"
   N_CLEAN=\$(echo \"\$OUT\" | grep -cF \"depends on axioms: $EXPECTED\" || true)
   if [ \"\$N_CLEAN\" -ne ${#CERTS[@]} ]; then
     echo \"AXIOM AUDIT FAILED: \$N_CLEAN/${#CERTS[@]} certificates clean\"
@@ -216,7 +216,7 @@ lake env bash -c "
   { echo 'import Proofs.SigApexSpec'; echo 'import Proofs.PointLiftSpec'; echo 'import Proofs.PointEqSpec'; echo 'import Proofs.DecompressMain'; echo '#print axioms CurveFieldProofs.verify_accepts_iff'; echo '#print axioms CurveFieldProofs.verify_accepts_iff_point'; echo '#print axioms CurveFieldProofs.verify_accepts_iff_point_eq'; echo '#print axioms CurveFieldProofs.verify_accepts_iff_decompress'; } > \"\$AUD\"
   OUT=\$(LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1)
   echo \"\$OUT\"
-  rm -f \"\$AUD\"
+  rm -f \"\$AUD\" \"\${AUD%.lean}.olean\"
   FLAT=\$(echo \"\$OUT\" | tr '\\n' ' ' | tr -s ' ')
   if echo \"\$FLAT\" | grep -qF \"'CurveFieldProofs.verify_accepts_iff' depends on axioms: \$ALLOWED\" \
      && echo \"\$FLAT\" | grep -qF \"'CurveFieldProofs.verify_accepts_iff_point' depends on axioms: \$ALLOWED\" \