Merge pull request #783 from viperproject/meilers_fix_proof_obligations

Fixing crash in proof obligation expression computation

Author: marcoeilers

src/main/scala/viper/silver/ast/utility/Expressions.scala

@@ -184,7 +184,7 @@ object Expressions {
           case _ => NoPosition
         }
         // Conditions for the current node.
-        val conds = n match {
+        val conds: Seq[Exp] = n match {
           case f@FieldAccess(rcv, _) => List(NeCmp(rcv, NullLit()(p))(p), FieldAccessPredicate(f, WildcardPerm()(p))(p))
           case f: FuncApp => prog.findFunction(f.funcname).pres
           case Div(_, q) => List(NeCmp(q, IntLit(0)(p))(p))
@@ -204,16 +204,16 @@ object Expressions {
         // Combine the conditions of the subnodes depending on what node we currently have.
         val finalSubConds = n match {
           case And(left, _) =>
-            val Seq(leftConds, rightConds) = nonTrivialSubConds
+            val Seq(leftConds, rightConds, Seq()) = nonTrivialSubConds
             reduceAndProofObs(left, leftConds, rightConds, p)
           case Implies(left, _) =>
-            val Seq(leftConds, rightConds) = nonTrivialSubConds
+            val Seq(leftConds, rightConds, Seq()) = nonTrivialSubConds
             reduceImpliesProofObs(left, leftConds, rightConds, p)
           case Or(left, _) =>
-            val Seq(leftConds, rightConds) = nonTrivialSubConds
+            val Seq(leftConds, rightConds, Seq()) = nonTrivialSubConds
             reduceOrProofObs(left, leftConds, rightConds, p)
           case CondExp(cond, _, _) =>
-            val Seq(condConds, thenConds, elseConds, _) = nonTrivialSubConds
+            val Seq(condConds, thenConds, elseConds, Seq()) = nonTrivialSubConds
             reduceCondExpProofObs(cond, condConds, thenConds, elseConds, p)
           case _ => subConds.flatten
         }