ernie cohen

Users who actually try the examples in VS Code will be confused when a comment disagrees with what they see when they hover. I think the first such example is...

Internal Error: System.NullReferenceException

1

### Dafny version 4.6.0 (nightly 4/17) ### Code to produce this issue ```dafny trait Ins { function step(s:State):State //requires safe?(s) } type Code = seq datatype State = S( clock:nat...

function refinement broken

2

### Dafny version 4.5.0, 4.6.0, nightly ### Code to produce this issue ```dafny abstract module A { function F(x: int): (r: int) ensures r > x } module B refines...

internal error on trait functions taking multiple arguments of trait type parameter

2

### Dafny version nightly 4/25/24 ### Code to produce this issue ```dafny newtype V = bv64 trait Op { //function op(t:T):T // no problem with this function op2(t0:T,t1:T):T // this...

### Dafny version nightly (4.6, 4/25) ### Code to produce this issue ```dafny datatype S = S( n:nat ) { function f():S { this } function g():S { this.(n :=...

internal error on match with static const of newtype

2

Failing code ------------ ``` newtype T = nat { static const C := 0 as T const V:bool := match this case C => true } ``` Steps to reproduce...

internal error on static constants in newtypes based on bitvectors

4

### Dafny version 4.6 ### Code to produce this issue ```dafny newtype T = bv1 { static const c := 0 as T } const c := T.c ``` ###...

Failing code ------------ ```dafny datatype D = D function f(d:D):bool { assert true by { match d { case _ => assert true; } } true } ``` Steps to...

Fragility issue when inherited trait function used in inherited contract

1

### Dafny version 4.7.0 ### Code to produce this issue ```dafny module Ma { trait {:termination false} A { ghost predicate has(d:int,b:bool) decreases this ghost predicate p(d:int) { forall b...

Rust compilation doesn't handle polymorphic static functions

1

### Dafny version 4.8.0 (nightly 9/6) ### Code to produce this issue ```dafny datatype F = F(t:T) { static function ctor(t:T):F { F(t) } } ``` ### Command to run...