dafny
dafny copied to clipboard
Crash in new resolver
The following program crashes the resolver
ghost function f2(items: set<nat>): (r:nat)
requires |items| > 0 {
var item :| item in items;
item
}
function f(items: set<nat>) : (r:nat)
requires |items| > 0 {
//assume exists item :: item in items && forall other <- items :: item == other || item < other;
//assert exists item Smallest()
var item :| IsSmallest(items, item);
item
}
predicate IsSmallest(s: set<nat>, item: nat)
requires item in s {
m in s && forall y: nat :: y in s ==> m <= y
}
lemma Smallest(s: set<nat>) returns (m: nat)
requires s != {}
ensures m in s && IsSmallest(s, m)
decreases s
{
m :| m in s;
if y: nat :| y in s && y < m {
ghost var s' := s - {m};
assert y in s';
m := ThereIsASmallest(s');
}
}
function smallest(items: set<nat>): (r: nat)
requires |items| > 0
method m(items: set<nat>) returns (r:nat)
requires |items| > 0 {
var item :| item in items;
return item;
}
results in:
Dafny encountered an internal error. Please report it at <https://github.com/dafny-lang/dafny/issues>.
System.InvalidCastException: Unable to cast object of type 'Microsoft.Dafny.UnusedPreType' to type 'Microsoft.Dafny.DPreType'.
at Microsoft.Dafny.PreTypeConstraints.ConfirmConstraint(CommonConfirmationBag check, PreType preType, DPreType auxPreType)
at Microsoft.Dafny.PreTypeConstraints.ConfirmTypeConstraints()
at Microsoft.Dafny.PreTypeConstraints.SolveAllTypeConstraints(String printableContext)
at Microsoft.Dafny.PreTypeResolver.ResolveFunction(Function f)
at Microsoft.Dafny.PreTypeResolver.ResolveMember(MemberDecl member)
at Microsoft.Dafny.PreTypeResolver.ResolveDeclarationBody(Declaration d)
at Microsoft.Dafny.PreTypeResolver.ResolveDeclarations(List`1 declarations, ModuleResolver resolver, Boolean firstPhaseOnly)
at Microsoft.Dafny.ModuleResolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, String moduleDescription, Boolean isAnExport)
at Microsoft.Dafny.ModuleDefinition.Resolve(ModuleSignature sig, ModuleResolver resolver, String exportSetName)
at Microsoft.Dafny.LiteralModuleDecl.Resolve(ModuleResolver resolver, CompilationData compilation)
at Microsoft.Dafny.ModuleResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl)
at Microsoft.Dafny.LanguageServer.Language.CachingResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl)
at Microsoft.Dafny.ProgramResolver.Resolve(CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.CachingResolver.<>c__DisplayClass5_0.<Resolve>b__0()
at Microsoft.Dafny.LanguageServer.Language.CachingResolver.Resolve(CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.RunDafnyResolver(Compilation compilation, Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.ResolveSymbols(Compilation compilation, Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.TextDocumentLoader.ResolveInternal(Compilation compilation, Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.TextDocumentLoader.<>c__DisplayClass5_0.<<ResolveAsync>b__0>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.TextDocumentLoader.ResolveAsync(Compilation compilation, Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.ResolveAsync()