Match error scala.MatchError: ? && true (of class viper.silver.ast.ImpreciseExp) that is occurring across the majority of the benchmark files generated for list.c0 seems to be caused by a translation issue in the frontend. When the corresponding .vpr file is run in the backend it verifies correctly. Further, I narrowed down the issue to a problem translating imprecise predicate bodies to a node that is in fact imprecise. I traced down the backend error and found that it is trying to case on a predicate body based on if it is precise or imprecise. However, the predicate body which should be imprecise is going into the precise case and creating the error.
Match error
scala.MatchError: ? && true (of class viper.silver.ast.ImpreciseExp)that is occurring across the majority of the benchmark files generated forlist.c0seems to be caused by a translation issue in the frontend. When the corresponding .vpr file is run in the backend it verifies correctly. Further, I narrowed down the issue to a problem translating imprecise predicate bodies to a node that is in fact imprecise. I traced down the backend error and found that it is trying to case on a predicate body based on if it is precise or imprecise. However, the predicate body which should be imprecise is going into the precise case and creating the error.