Branching und unfolds looking good now.

src/main/scala/biabduction/BiAbduction.scala

@@ -109,11 +109,10 @@ case class LoopInvariantSuccess(s: State, v: Verifier, invs: Seq[Exp] = Seq(), l
   def addToMethod(m: Method): Option[Method] = {
     val body = m.body.get
     val newBody = body.transform {
-      case l: While if l == loop =>
+      case l: While if l.cond == loop.cond =>
         l.copy(invs = l.invs ++ invs)(pos = l.pos, info = l.info, errT = l.errT)
       case other => other
     }
-    //val newBody = body.copy(ss = newSs)(pos = body.pos, info = body.info, errT = body.errT)
     Some(m.copy(body = Some(newBody))(pos = m.pos, info = m.info, errT = m.errT))
   }
 }
@@ -124,7 +123,6 @@ case class FramingSuccess(s: State, v: Verifier, posts: Seq[Exp], loc: Position)
   def addToMethod(m: Method): Option[Method] = {
     Some(m.copy(posts = m.posts ++ posts)(pos = m.pos, info = m.info, errT = m.errT))
   }
-
 }
 
 case class BiAbductionFailure(s: State, v: Verifier) extends BiAbductionResult {
@@ -298,7 +296,11 @@ object abductionUtils {
   }
 
   def getContainingPredicates(f: FieldAccess, p: Program): Seq[Predicate] = {
-    p.predicates.filter(_.body.get.contains(f))
+
+    p.predicates.filter{ pred =>
+      val absAcc = f.copy(rcv = pred.formalArgs.head.localVar)(f.pos, f.info, f.errT)
+      pred.body.get.contains(absAcc)
+    }
   }
 
   def checkBc(v: Verifier, bc: Term, ignoredBcs: Seq[Term]): Boolean = {

src/main/scala/rules/Executor.scala

@@ -360,7 +360,7 @@ object executor extends ExecutionRules {
     }
   }
 
-  private def checkInvariants(s: State, v: Verifier, invs: Seq[Exp], stmt: Stmt)(Q: (State, Verifier) => VerificationResult): VerificationResult = {
+  private def checkInvariants(s: State, v: Verifier, invs: Seq[Exp], location: Stmt)(Q: (State, Verifier) => VerificationResult): VerificationResult = {
     if (invs.isEmpty) {
       Q(s, v)
     } else {
@@ -372,7 +372,7 @@ object executor extends ExecutionRules {
       } {
         f =>
         // There are cases where it is incorrect to abduce state here, but only some cases and it is hard to distinguish them
-        BiAbductionSolver.solveAbduction(s, v, f, Some(stmt))((s3, res, v3) => Success(Some(res)) && checkInvariants(s3, v3, invs, stmt)(Q))
+        BiAbductionSolver.solveAbduction(s, v, f, Some(location))((s3, res, v3) => Success(Some(res)) && checkInvariants(s3, v3, invs, location)(Q))
       }
     }
   }

src/main/scala/supporters/MethodSupporter.scala

@@ -132,12 +132,12 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent {
 
       val abdResult: VerificationResult = result match {
         case suc: NonFatalResult if method.body.isDefined =>
+
           // Collect all the abductions and try to generate preconditions
           val abdReses = abductionUtils.getBiAbductionSuccesses(suc)
-
-
-          val pres = abductionUtils.getAbductionSuccesses(suc).filter{_.state.nonEmpty}
-
+          val pres = abductionUtils.getAbductionSuccesses(suc).collect{ case abd if abd.state.nonEmpty => abd}
+          val states = pres.map(_.state.head)
+          val triggers = pres.map(_.trigger)
           val newMethod = abdReses.foldLeft[Option[Method]](Some(method))( (m, res) => m match {
             case None => 
               None
@@ -177,7 +177,6 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent {
         consumes(s, posts, postViolated, v)(QS)
       } {
         (s1: State, _: Term, v1: Verifier) => {
-          // TODO nklose We want to do abstraction, but that might require adding folds and such...
           BiAbductionSolver.solveAbstraction(s1, v1) { (s2, framedPosts, v2) =>
             val formals = method.formalArgs.map(_.localVar) ++ method.formalReturns.map(_.localVar)
             val vars = s2.g.values.collect { case (var2, t) if formals.contains(var2) => (var2, t) }