Stefan Zetzsche comments

Results 6 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.

Test generation cannot find witness for type nat

Temporary workaround was merged in https://github.com/dafny-lang/dafny/pull/5609. Does not fix the underlying issue.

Bad encoding for `this` in tail recursive functions when compiling to Java

Can confirm that running above code with java as target throws an error (error: local variables referenced from a lambda expression must be final or effectively final).