diff --git a/progs/VSUpile/verif_stdlib.v b/progs/VSUpile/verif_stdlib.v
index 7130f8763..4f5349420 100644
--- a/progs/VSUpile/verif_stdlib.v
+++ b/progs/VSUpile/verif_stdlib.v
@@ -10,8 +10,11 @@ Lemma version_test: False.
          VST.veric.version.compcert_version = "3.13"%string /\
 	       stdlib.Info.version = "3.12"%string \/
          VST.veric.version.compcert_version = "3.13"%string /\
-	       stdlib.Info.version = "3.11"%string) by (compute; auto).
- assert (VST.veric.version.bitsize = stdlib.Info.bitsize) by reflexivity.
+	       stdlib.Info.version = "3.11"%string)
+       by (compute; auto;
+            match goal with |- ?G => fail 100 "Version mismatch; cannot prove" G end).
+ assert (VST.veric.version.bitsize = stdlib.Info.bitsize) by
+    (try reflexivity; match goal with |- ?G => fail 100 "Bitsize mismatch; cannot prove" G end).
 Abort.
 
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.