viperproject/silicon

Let expression in forall body causes exception

Felalolf opened this issue · 2 comments

Felalolf commented

The following Viper Snipet causes Silicon to crash with "java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: java.lang.RuntimeException: Unexpected expression acc(y.f, write) cannot be symbolically evaluated".

field f: Int

method bar(x: Seq[Ref]) 
  requires forall i: Int, j: Int :: 0 <= i && i < |x| && 0 <= j && j < |x| && i != j ==> x[i] != x[j]
  requires forall i: Int :: 0 <= i && i < |x| ==> let y == (x[i]) in acc(y.f) // fails
  requires forall i: Int :: 0 <= i && i < |x| ==>  let y == (x[i]) in y.f >= 5 // ok

I get the error in the IDE and also when verifying corresponding Viper AST nodes directly.

Felalolf commented

The same happens with carbon, see viperproject/carbon#430

Felalolf commented

I have attached the stack trace I get when verifying a let expression in a forall body with Gobra:
log.txt