trait SomeTrait<T> {
function f(): (res: T)
}
// doesn't terminate:
// class Bar {}
type Bar = nat
// terminates:
// type {:extern} Bar
// datatype Bar = Bar
// hangs:
datatype Option<+U> = None | Some(val: U)
// terminates:
// datatype Option<U> = None | Some(val: U)
method foo(v: Option<SomeTrait<Bar>>)
{
var _ := match v {
case Some(s) => Some(s.f())
case _ => None
};
}
The above command does not seem to terminate. Changing to any of the commented out options for Bar or changing the variance for Options type parameter from +U to U makes the program resolve successfully.
What type of operating system are you experiencing the problem on?
Dafny version
4.6.0+7c82175da631d3fdc3acea92a3614d66a3fdf7f2
Code to produce this issue
Command to run and resulting output
What happened?
The above command does not seem to terminate. Changing to any of the commented out options for
Bar
or changing the variance forOption
s type parameter from+U
toU
makes the program resolve successfully.What type of operating system are you experiencing the problem on?
Linux, Mac