search

dafny-lang / dafny

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

Standard libraries not working with general-newtypes=true #5345

Closed MikaelMayer closed 6 months ago

MikaelMayer commented 6 months ago

Dafny version

latest-nightly

Code to produce this issue

# dfyconfig.toml

[options]
standard-libraries=true
type-system-refresh=true
general-newtypes=true

Command to run and resulting output

> dafny verify dfyconfig.toml

DafnyStandardLibraries.dfy(4398,14): Error: type conversion to a char type is al
lowed only from numeric and bitvector types, char, and ORDINAL (got bv6)
     |
4398 |       (i - 4) as char
     |               ^^

What happened?

There should have been no errors from the standard library. This error is preventing me from using newtypes in my application that requires the standard library.

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

Windows

RustanLeino commented 6 months ago

With --general-newtypes, the conversion has to go via int:

(i - 4) as int as char