## [wp] non-provable local typing constraints in lemmas

# Steps to reproduce the issue

The attached archive contains the ACSL function `Count`

together with several lemma.
Also contained are

- a Makefile
- a coq proof in file
`wp0.script.20`

for lemma`CountBounds`

that works for Frama-C 20 - an attempt of a coq proof in file
`wp0.script.21`

for lemma`CountBounds`

that fails for Frama-C 21 - The files
`CountBounds.v.20`

and`CountBounds.v.21`

contain the coq code as extracted from CoqIde

# Expected behaviour

My problem is that I am unable to adapt the coq proof that worked fro Frama-C 20 to the newer version of Frama-C.

# Actual behaviour

I suspect that this is related to changes in the generated Coq code of the VC of lemma `CountBounds`

This can be best seen when calling `diff CountBounds.v.20 CountBounds.v.21`

.

```
$ diff CountBounds.v.20 CountBounds.v.21
39,40c39,40
< (((t.[ (shift_sint32 a x) ]) <> i_2)%Z) -> ((i < i_1)%Z) ->
< ((is_sint32 i_2%Z)) ->
---
> let x_1 := (t.[ (shift_sint32 a x) ])%Z in ((x_1 <> i_2)%Z) ->
> ((i < i_1)%Z) -> ((is_sint32 i_2%Z)) -> ((is_sint32 x_1)) ->
```

# Fix ideas

I think the issue is caused by the condition `((is_sint32 x_1))`

for the newly introduced term `x_1 := (t.[ (shift_sint32 a x) ])%Z`

. I haven't found a way to satisfy the condition `((is_sint32 x_1))`

and I suspect that it is not possible.
If it is possible, then I apologise and ask for a hint.

Regards

Jens Gerlach

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information