Exhale QPs with predicates results in an "empty.reduceLeft" error

[tdardinier]

The Viper program

predicate p()

method m()
  ensures forall i: Int :: p()

results in the following error:

ERROR: The following exception occured in ViperServer: java.lang.UnsupportedOperationException: empty.reduceLeft
 trace:
  scala.collection.TraversableOnce.reduceLeft(TraversableOnce.scala:179)
  scala.collection.TraversableOnce.reduceLeft$(TraversableOnce.scala:177)
  scala.collection.mutable.ArrayBuffer.scala$collection$IndexedSeqOptimized$$super$reduceLeft(ArrayBuffer.scala:47)
  scala.collection.IndexedSeqOptimized.reduceLeft(IndexedSeqOptimized.scala:73)
  scala.collection.IndexedSeqOptimized.reduceLeft$(IndexedSeqOptimized.scala:72)
  scala.collection.mutable.ArrayBuffer.reduceLeft(ArrayBuffer.scala:47)
  scala.collection.TraversableOnce.reduce(TraversableOnce.scala:207)
  scala.collection.TraversableOnce.reduce$(TraversableOnce.scala:207)
  scala.collection.AbstractTraversable.reduce(Traversable.scala:104)
  viper.carbon.modules.impls.QuantifiedPermModule.translateExhale(QuantifiedPermModule.scala:723)

which occurs because a reduce operation is done on the arguments of the predicates, and in this case the predicate has no argument.

This should probably be handled by the consistency checks.

[tdardinier]

Corresponding Silicon issue

[mschwerhoff]

Resolved in Silicon with PR viperproject/silicon#597.

Corresponding regression in PR viperproject/silver#554. The latter should only be accepted once this Carbon is was resolved.

[JonasAlaif]

It seems that the Silver regression PR viperproject/silver#554 was merged without a fix in Carbon. I'll disable this test (all/issues/silicon/0595.vpr) in Silver for Carbon for now, but it should be reenabled once this is fixed.

[alexanderjsummers]

I can't reproduce the error in Carbon (I get a well-definedness error, but I think that's correct with the latest design)

[marcoeilers]

This no longer got us the error shown above, but resulted in Boogie code with quantifiers with no quantified variables, which led to a Boogie error. Fixed in PR #541.