Nicolas Voirol

Yeah that looks like the Inox issue I mentioned. I expect that the example using a pair instead of the `B` type works because the counterexample is found before the...

Probably some bug in type encoding (which triggers because the type arguments aren't bijective in `Commutative[A] extends Forall[(A,A)]`). What does the crash say?

Hmm, why does this fail the well-formedness check?

Hmm, so `holdsFor` is the broken method in that snippet. Do you also have a failing well-formedness check for `apply`? We would need to see the definition of `holdsFor` generated...

I must be missing something. In the above trees, I would expect the definitions of `apply` and `holdsFor` dispatchers to correctly type-check, no? In the branch where the type-checking fails,...

No these aren't really existentials but rather "erased" types with bounds. The idea is that we can lose a bit of precision at the type level since the semantics are...

I'm pretty sure Z3 and CVC4 support floating-point arithmetic. Why not add solver support?

The SMT standard [1] has support for FP BV conversions but it seems like the -> direction is not injective (which might break your `doubleToRawLongBits` post-condition). They recommend using ```...

The problem is ADT constructor types don't exist in SMT world so we have to encode `FunType` into `{x: Type | x is FunType }`. The way Inox handles refinement...

Regis wrote up an example with an `SFun` case class which does something similar: https://github.com/epfl-lara/stainless/blob/a041c9790d24411f45c4329526adec334bc71337/frontends/benchmarks/imperative/valid/Tutorial.scala#L192-L194