Search results

New resolver produces Boogie error

during 2: compilation of correct programDafny rejects a valid program during compilationDafny rejects a valid program during compilation

part: resolverResolution and typecheckingResolution and typechecking

Status: Open.

Bug

#6364 In dafny-lang/dafny;

· keyboardDrummer opened on Sep 17, 2025

Opaque blocks prove variable previously assigned

during 3: execution of incorrect programAn bug in the verifier that allows Dafny to run a program that does not correctly implement its specAn bug in the verifier that allows Dafny to run a program that does not correctly implement its spec

kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labelCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Status: Open.

#6363 In dafny-lang/dafny;

· MikaelMayer opened on Sep 16, 2025

Type synonyms in <code>least</code>/<code>greatest</code> lemmas

kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labelCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Status: Open.

#6360 In dafny-lang/dafny;

· volodeyka opened on Sep 5, 2025

Getting invariant to pass requires repeating a subexpression of it

incompletenessThings that Dafny should be able to prove, but can'tThings that Dafny should be able to prove, but can't

Status: Open.

#6356 In dafny-lang/dafny;

· keyboardDrummer opened on Sep 2, 2025

Dafny assumes non-termination for a loop it cannot prove termination

kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labelCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Status: Open.

#6355 In dafny-lang/dafny;

· TomSMaier opened on Sep 1, 2025

Simple program does not verify automatically

incompletenessThings that Dafny should be able to prove, but can'tThings that Dafny should be able to prove, but can't

Status: Open.

#6354 In dafny-lang/dafny;

· keyboardDrummer opened on Sep 1, 2025

Missing export-provides causes crash

kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labelCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

part: resolverResolution and typecheckingResolution and typechecking

Status: Open.

#6351 In dafny-lang/dafny;

· RustanLeino opened on Aug 29, 2025

Crash when named class constructor is used inside match case

kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labelCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

part: resolverResolution and typecheckingResolution and typechecking

Status: Open.

#6345 In dafny-lang/dafny;

· RustanLeino opened on Aug 25, 2025

Soundness issue when variable present in function postcondition with recursive call with same arguments

during 3: execution of incorrect programAn bug in the verifier that allows Dafny to run a program that does not correctly implement its specAn bug in the verifier that allows Dafny to run a program that does not correctly implement its spec

kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labelCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Status: Open.

#6343 In dafny-lang/dafny;

· samuelchassot opened on Aug 22, 2025

Crash and scope issue with <code>var x := e by { ... }</code>

crashDafny crashes on this input, or generates malformed code that can not be executedDafny crashes on this input, or generates malformed code that can not be executed

kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labelCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

part: resolverResolution and typecheckingResolution and typechecking

part: verifierTranslation from Dafny to Boogie (translator)Translation from Dafny to Boogie (translator)

Status: Open.

#6342 In dafny-lang/dafny;

· RustanLeino opened on Aug 20, 2025

Binding guard assumes type condition too early

during 3: execution of incorrect programAn bug in the verifier that allows Dafny to run a program that does not correctly implement its specAn bug in the verifier that allows Dafny to run a program that does not correctly implement its spec

kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labelCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Status: Open.

#6341 In dafny-lang/dafny;

· RustanLeino opened on Aug 20, 2025

SinglePassCodeGenerator produces init calls inconsistent with standard library externs

has-workaround: yesThere is a known workaroundThere is a known workaround

invalid translated codeThe compiler generates invalid code, making the the target language infrastructure crashThe compiler generates invalid code, making the the target language infrastructure crash

kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labelCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

lang: c#Dafny's C# transpiler and its runtimeDafny's C# transpiler and its runtime

lang: c++Dafny's C++ transpiler and its runtimeDafny's C++ transpiler and its runtime

lang: golangDafny's transpiler to Go and its runtimeDafny's transpiler to Go and its runtime

lang: javaDafny's Java transpiler and its runtimeDafny's Java transpiler and its runtime

lang: jsDafny's JavaScript transpiler and its runtimeDafny's JavaScript transpiler and its runtime

lang: pythonDafny's Python transpiler and its runtimeDafny's Python transpiler and its runtime

lang: rustDafny's transpiler to Rust and its runtimeDafny's transpiler to Rust and its runtime

part: code-generationSupport for transpiling Dafny to another language. If relevant, add a `lang:` tagSupport for transpiling Dafny to another language. If relevant, add a `lang:` tag

Status: Open.

Bug

#6333 In dafny-lang/dafny;

· ssomayyajula opened on Aug 17, 2025