Jad Hamza

Results 55 comments of Jad Hamza

Incorrect universe constraints declared for inductive type

Thanks! Yes it works with `noind` both for this example and #240

Better error messages for transitively mutable classes

Here I think the error is that you need to annotate `@mutable trait C {}`, and then you'll have other error messages.

Better error messages for transitively mutable classes

> yes, sorry, to be clearer, the issue is that once you put the @mutable annotation on C. you inherit (ho ho ho) two problems. the first is that the...

Strange timing for valid VCs in portfolio mode with timeout

I checked again by running just with `--solvers=smt-cvc4`, and `CVC4` is in fact able to solve the VC instantly (so last sentence of previous post was wrong). But for some...

Strange timing for valid VCs in portfolio mode with timeout

Fixed in https://github.com/epfl-lara/inox/pull/134

Casts to ensure identical types?

I think they come from here, we can avoid generating the assertion when there is just one constructor: https://github.com/epfl-lara/stainless/blob/940261c8669beba76cff59fc05eea2ddfd4a6988/core/src/main/scala/stainless/verification/AssertionInjector.scala#L79-L85

Casts to ensure identical types?

If we add `Unchecked` the type-checker will also ignore assertions that appear in `expr` (I guess we have this problem in other places where we use `Unchecked`)

Casts to ensure identical types?

At the moment let bindings don't work well with `SizedADT` because `getType` returns `ADT`

Casts to ensure identical types?

Yes that'd be great, but these are big changes, what do you have in mind? Should `SizedADT` be moved to Inox?

Casts to ensure identical types?

This is fixed now by I'm reopening for the untyped let-binding and the `Unchecked` annotation.