Hichem R. A.
Hichem R. A.
Yes it can be done that way. Or the ones that don't pass can be put in a folder named `unknown` and I am not sure but I think that...
Yes, I agree, the ones that pass (I think two of them do) can be put in the non-regression tests as valid, the others should be moved to marvin. Regarding...
Yes, sorry, all good by me.
We can probably generate a good amount of them from Why3's test-suite. Also once printers become available in Dolmen we can translate some of them. But I think it should...
I think its worth adding a test with `forall _: x. forall _: y. exist ...` to make sure that the behavior is correct in this case as well. I...
IIRC it was used on function and value names, not on theory symbols, AFAIK the shadowing of theory symbols is not allowed in the SMT-LIB standard.
This is probably due to the fact that ocaml-solidity supports only the versions 0.6.x (cf. https://ocamlpro.com/blog/2020_05_19_ocaml_solidity_parser_with_menhir/) of solidity while that contract is written in 0.8.0. After testing I got the...
The theory of integers is supposed to handle mathematical/arbitrary sized integers, so bit-wise reasoning is usually not included in theories of integers (https://smt-lib.org/theories-Ints.shtml). Afaik smt solvers use something like Zarith/GMP...
No problem, I just changed it.
Looks like something with the new change significantly slows down the CI, I can change it back, or maybe we should investigate more in case in it a bug.