search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.94k stars 263 forks source link

bitvector rotation operations sometimes reported nonexisting by incremental resolver #5830

Open erniecohen opened 1 month ago

erniecohen commented 1 month ago

Dafny version

4.8.1

Code to produce this issue

const c := (1 as bv64).RotateRight(1)

Command to run and resulting output

dfyconfig.toml with

general-traits = "datatype"
type-system-refresh = "true"
general-newtypes = "true"

What happened?

To repro, 1) restart dafny; code verifies 2) add a newline to the whitespace of the file; resolver now reports "member 'RotateRight" does not exist in type 'bv64'

What type of operating system are you experiencing the problem on?

Mac