Stefan Zetzsche comments

Repositories
Issues
Comments

Results 4 comments of


                                            Stefan Zetzsche

Type checking sometimes doesn't terminate when using `--type-system-refresh`

I can confirm the behaviour on my Mac in VSCode with Dafny 4.6.0.

`fresh` doesn't imply inequality with `--general-traits=datatype`

I can confirm that `--type-system-refresh` has an effect on the verification result. What is your take on this @RustanLeino?

Prover died on simple program

This seems to be caused by the trigger. If I run the program without verifying it, I get this boogie translation error: `Error: trigger must mention all quantified variables, but...

internal error on static constants in newtypes based on bitvectors

Closing this issue as I can't reproduce it either. Feel free to push again if needed.