boogie with type errors generated on verification

[erniecohen]

Failing code

module m {
trait Set<S> {
    function v(s:S):set<int> // abstract value
    predicate has(s:S,t:int) decreases 0,this ensures has(s,t) <==> t in v(s) 
}
datatype SetC = SetC(rep:set<int>) {
    function v():set<int> { rep }
    predicate has(t:int) decreases 0 { t in rep }
}
trait SetStaticC extends Set<SetC> {
    function v(s:SetC):set<int> { s.v() }
    predicate has(s:SetC,t:int) ensures has(s,t) <==> t in v(s) { s.has(t) }
}
}

Steps to reproduce the issue

• Dafny version: 4.7.0.0 build of 8/3
• Dafny VSCode extension version: 3.3.1

Expected behavior

not crashing

Actual behavior

(6 errors, starting with the following)
Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.ArgumentException: Boogie program had 2 type errors:
Microsoft.Dafny.BoogieRangeToken: invalid argument types (Box and ref) to binary operator ==
Microsoft.Dafny.BoogieRangeToken: invalid argument types (Box and ref) to binary operator !=
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass54_0.<b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func2 taskFilter, Nullable1 randomSeed)