I have a plan now

src/main/scala/biabduction/BiAbduction.scala

@@ -114,7 +114,7 @@ trait BiAbductionRule[S] {
 // TODO nklose can we move this all into happening for consumes only?
 object BiAbductionSolver {
 
-  def solveAbduction(s: State, v: Verifier, goal: Seq[Exp], tra: Option[AbductionQuestionTransformer], loc: Position): BiAbductionResult = {
+  def solveAbduction(s: State, v: Verifier, goal: Seq[Exp], tra: Option[AbductionQuestionTransformer], loc: Position): Seq[BiAbductionResult] = {
 
     val res = executionFlowController.locally(s, v)((s1, v1) => {
 
@@ -136,10 +136,9 @@ object BiAbductionSolver {
 
     res match {
       case nf: NonFatalResult =>
-        // TODO Can we ever get multiple abduction results here?
-        abductionUtils.getAbductionResults(nf).head
+        abductionUtils.getAbductionResults(nf)
       case _ =>
-        BiAbductionFailure(s, v)
+        Seq(BiAbductionFailure(s, v))
     }
   }
 

src/main/scala/interfaces/Verification.scala

@@ -108,7 +108,7 @@ case class Failure/*[ST <: Store[ST],
 case class SiliconFailureContext(branchConditions: Seq[ast.Exp],
                                  counterExample: Option[Counterexample],
                                  reasonUnknown: Option[String],
-                                 abductionResult: Option[BiAbductionResult]) extends FailureContext {
+                                 abductionResult: Option[Seq[BiAbductionResult]]) extends FailureContext {
 
   lazy val branchConditionString: String = {
     if (branchConditions.nonEmpty) {

src/main/scala/rules/ChunkSupporter.scala

@@ -140,6 +140,10 @@ object chunkSupporter extends ChunkSupportRules {
             case _ if v1.decider.checkSmoke(true) =>
               Success() // TODO: Mark branch as dead?
             case _ =>
+
+              // TODO nklose: we should move abduction out of createFailure to here and then just recurse with the results
+              // This should also replace the result handling in executor and consumer
+              // We can then do the abduction on the "original" state s, not the partial heap h
               createFailure(ve, v1, s1, "consuming chunk", true)
           }
         }

src/main/scala/rules/Consumer.scala

@@ -6,16 +6,9 @@
 
 package viper.silicon.rules
 
-import viper.silicon.debugger.DebugExp
 import viper.silicon.Config.JoinMode
-
-import scala.collection.mutable
-import viper.silver.ast
-import viper.silver.ast.utility.QuantifiedPermissions.QuantifiedPermissionAssertion
-import viper.silver.verifier.PartialVerificationError
-import viper.silver.verifier.reasons._
-import viper.silicon.interfaces.VerificationResult
 import viper.silicon.biabduction.{AbductionSuccess, BiAbductionFailure}
+import viper.silicon.debugger.DebugExp
 import viper.silicon.interfaces.{Failure, SiliconFailureContext, Success, VerificationResult}
 import viper.silicon.logger.records.data.{CondExpRecord, ConsumeRecord, ImpliesRecord}
 import viper.silicon.state._
@@ -186,16 +179,18 @@ object consumer extends ConsumptionRules {
     res match {
       case f@Failure(ve, _) if abductionLocation.isDefined =>
         ve.failureContexts.head.asInstanceOf[SiliconFailureContext].abductionResult match {
-          case Some(as: AbductionSuccess) => {
+          case Some((as: AbductionSuccess) :: rest ) => {
+            // Current assumption: we always do this recursively up the stack, so we only have to do the head
             producer.produces(s, freshSnap, as.state, ContractNotWellformed, v) { (s1, v1) =>
               executor.execs(s1, as.stmts.reverse, v1) { (s2, v2) =>
                 // TODO nklose this is not working. The abduced heap chunk is not being consumed
-                wrappedConsumeTlc(s2, s2.h, a, pve, v2, abductionLocation)(Q) && Success(Some(as.copy(loc = abductionLocation.get)))
+                val restSuc = rest.foldLeft[VerificationResult](Success()){ case (suc, abs: AbductionSuccess) => suc && Success(Some(abs.copy(loc = abductionLocation.get))) }
+                restSuc && Success(Some(as.copy(loc = abductionLocation.get))) && wrappedConsumeTlc(s2, s2.h, a, pve, v2, abductionLocation)(Q)
               }
             }
           }
-          case Some(_: BiAbductionFailure) =>
-            println("Abduction failed")
+          case Some(Seq(_: BiAbductionFailure)) =>
+            //println("Abduction failed")
             f
         }
       case res => res

src/main/scala/rules/Executor.scala

@@ -767,21 +767,25 @@ object executor extends ExecutionRules {
            | _: ast.While => sys.error(s"Unexpected statement (${stmt.getClass.getName}): $stmt")
     }
 
+    // TODO nklose: make everything happen in consume, nothing here.
     executed match {
+
       case Failure(_: PostconditionViolated, _) => executed // Postconditions are handled elsewhere, we do not want to restart for them
       case Failure(ve, _) if ve.failureContexts.nonEmpty =>
-        ve.failureContexts.head.asInstanceOf[SiliconFailureContext].abductionResult match {
-          case Some(as: AbductionSuccess) =>
+        val abReses = ve.failureContexts.head.asInstanceOf[SiliconFailureContext].abductionResult.get
+        abReses.head match {
+          case as: AbductionSuccess =>
             producer.produces(s, freshSnap, as.state, ContractNotWellformed, v) { (s1, v1) =>
               executor.execs(s1, as.stmts.reverse, v1) { (s2, v2) =>
-                exec(s2, stmt, v2)((s3, v3) => Q(s3, v3) && Success(Some(as)))
+                val restSuc = abReses.tail.foldLeft[VerificationResult](Success()){ case (suc, abs: AbductionSuccess) => suc && Success(Some(abs.copy(loc = stmt.pos))) }
+                restSuc && Success(Some(as)) && exec(s2, stmt, v2)((s3, v3) => Q(s3, v3))
               }
-    }
+            }
 
-          case Some(_: BiAbductionFailure) =>
-            println("Abduction failed")
-    executed
-  }
+          case _: BiAbductionFailure =>
+            //println("Abduction failed")
+            executed
+        }
       case _ => executed
     }
   }