From ca88716f84e1a6a97341c61b1958433dbc8637c8 Mon Sep 17 00:00:00 2001 From: Jan-Oliver Kaiser Date: Wed, 2 Sep 2026 13:21:03 +0200 Subject: [PATCH] Adapt to SkyLabsAI/auto#412 --- rocq-brick-libstdcpp/test/cstring/proof.v | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/rocq-brick-libstdcpp/test/cstring/proof.v b/rocq-brick-libstdcpp/test/cstring/proof.v index afbeab67..9720ee2b 100644 --- a/rocq-brick-libstdcpp/test/cstring/proof.v +++ b/rocq-brick-libstdcpp/test/cstring/proof.v @@ -393,14 +393,16 @@ Section with_cpp. Lemma test_strchr_ok : verify[source] "test_strchr()". Proof. verify_spec; go. - all: simpl in *; by normalize_ptrs. + all: simpl in *; Arith.arith_simpl; normalize_ptrs; go. + all: by exfalso. Qed. cpp.spec "test_strrchr()" from source default. Lemma test_strrchr_ok : verify[source] "test_strrchr()". Proof. verify_spec; go. - all: simpl in *; by normalize_ptrs. + all: simpl in *; Arith.arith_simpl; normalize_ptrs; go. + all: by exfalso. Qed. cpp.spec "test_strspn()" from source default. @@ -415,16 +417,16 @@ Section with_cpp. Lemma test_strpbrk_ok : verify[source] "test_strpbrk()". Proof. verify_spec; go. - exfalso. - by normalize_ptrs. + all: Arith.arith_simpl; normalize_ptrs; go. + all: by exfalso. Qed. cpp.spec "test_strstr()" from source default. Lemma test_strstr_ok : verify[source] "test_strstr()". Proof. verify_spec; go. - all: exfalso. - all: by normalize_ptrs. + all: Arith.arith_simpl; normalize_ptrs; go. + all: by exfalso. Qed. cpp.spec "test_cstring_slice1()" from source default.