diff --git a/src/main/scala/biabduction/BiAbduction.scala b/src/main/scala/biabduction/BiAbduction.scala
index f5d81d2cc..2c19d9992 100644
--- a/src/main/scala/biabduction/BiAbduction.scala
+++ b/src/main/scala/biabduction/BiAbduction.scala
@@ -346,7 +346,7 @@ object BiAbductionSolver {
         case Some(t: Stmt) if t == abductionUtils.dummyEndStmt =>
           val newBody = addToInnerBody(body, finalStmt)
           val infPos = LineColumnPosition(m.pos.asInstanceOf[SourcePosition].end.get.line, m.pos.asInstanceOf[SourcePosition].end.get.column)
-          val infRes = finalStmt.map(stmt => "  " + ProgramEdit(infPos, infPos, stmt.toString() + "\n"))
+          val infRes = finalStmt.map(stmt => ProgramEdit(infPos, infPos, "  " + stmt.toString() + "\n"))
           (newBody, infRes)
 
         case Some(t: Stmt) if abductionUtils.isEndOfLoopStmt(t) =>
@@ -356,7 +356,7 @@ object BiAbductionSolver {
           val newBody = body.transform { case stmt if stmt == loop => newLoop }
 
           val infPos = LineColumnPosition(loop.pos.asInstanceOf[SourcePosition].end.get.line, loop.pos.asInstanceOf[SourcePosition].end.get.column)
-          val infRes = finalStmt.map(stmt => "  " + ProgramEdit(infPos, infPos, stmt.toString() + "\n"))
+          val infRes = finalStmt.map(stmt => ProgramEdit(infPos, infPos, "  " + stmt.toString() + "\n"))
           (newBody, infRes)
 
         case Some(t: Stmt) =>
diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala
index 850157fd0..579711464 100644
--- a/src/main/scala/supporters/MethodSupporter.scala
+++ b/src/main/scala/supporters/MethodSupporter.scala
@@ -167,13 +167,13 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent {
           val allEdits = mAbd.map(_._2).getOrElse(Seq()) ++ generateLoopInvFixes(loopInvReses) ++ mInv.map(m2 => generatePostFixes(m2, framingReses)).getOrElse(Seq())
 
           mFrame match {
-            case None => Failure(Internal(reason = InternalReason(DummyNode, "Resolving Biabduction results failed")))
+            case None => Failure(Internal(reason = InternalReason(method, "Resolving Biabduction results failed")))
             case Some(m) =>
               println("Original method: \n" + method.toString + "\nAbduced method: \n" + m.toString + "\nEdits: \n" + allEdits.mkString("\n"))
               val sNoAbd = sInit.copy(doAbduction = false)
               verify(sNoAbd, m) match {
                 case Seq(_: NonFatalResult) =>
-                  val error = Internal(DummyReason)
+                  val error = Internal(offendingNode = method, reason = InternalReason(method, "Inference successful"))
                   error.failureContexts = Seq(SiliconAbductionFailureContext(None, Some(allEdits)))
                   // We report an error with the fixes because fixes currently can only be contained in errors.
                   Failure(error)