diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/MethodConversionContext.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/MethodConversionContext.kt
index 5befe01847b6c..e7fed62ef8ca8 100644
--- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/MethodConversionContext.kt
+++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/MethodConversionContext.kt
@@ -40,12 +40,13 @@ interface MethodConversionContext : ProgramConversionContext {
     fun resolveLocal(name: Name): VariableEmbedding
     fun registerLocalProperty(symbol: FirPropertySymbol)
     fun registerLocalVariable(symbol: FirVariableSymbol<*>)
-    fun resolveReceiver(isExtension: Boolean): ExpEmbedding?
+    fun resolveDispatchReceiver(): ExpEmbedding?
+    fun resolveExtensionReceiver(labelName: String): ExpEmbedding?
 
     fun <R> withScopeImpl(scopeDepth: Int, action: () -> R): R
     fun addLoopIdentifier(labelName: String, index: Int)
     fun resolveLoopIndex(name: String): Int
-    fun resolveNamedReturnTarget(sourceName: String): ReturnTarget?
+    fun resolveNamedReturnTarget(labelName: String): ReturnTarget?
 }
 
 fun MethodConversionContext.resolveReturnTarget(targetSourceName: String?): ReturnTarget =
diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/MethodConverter.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/MethodConverter.kt
index bec890d78f4b9..660796cec4a26 100644
--- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/MethodConverter.kt
+++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/MethodConverter.kt
@@ -62,11 +62,13 @@ class MethodConverter(
         paramResolver.tryResolveParameter(name) ?: parent?.resolveParameter(name)
         ?: throw IllegalArgumentException("Parameter $name not found in scope.")
 
-    override fun resolveReceiver(isExtension: Boolean): ExpEmbedding? =
-        paramResolver.tryResolveReceiver(isExtension) ?: parent?.resolveReceiver(isExtension)
+    override fun resolveDispatchReceiver(): ExpEmbedding? =
+        paramResolver.tryResolveDispatchReceiver() ?: parent?.resolveDispatchReceiver()
+
+    override fun resolveExtensionReceiver(labelName: String): ExpEmbedding? =
+        paramResolver.tryResolveExtensionReceiver(labelName) ?: parent?.resolveExtensionReceiver(labelName)
 
     override val defaultResolvedReturnTarget = paramResolver.defaultResolvedReturnTarget
-    override fun resolveNamedReturnTarget(sourceName: String): ReturnTarget? {
-        return paramResolver.resolveNamedReturnTarget(sourceName) ?: parent?.resolveNamedReturnTarget(sourceName)
-    }
+    override fun resolveNamedReturnTarget(labelName: String): ReturnTarget? =
+        paramResolver.resolveNamedReturnTarget(labelName) ?: parent?.resolveNamedReturnTarget(labelName)
 }
\ No newline at end of file
diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ParameterResolver.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ParameterResolver.kt
index 60e2ce806c534..cafdd12a93fc8 100644
--- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ParameterResolver.kt
+++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ParameterResolver.kt
@@ -19,35 +19,38 @@ import org.jetbrains.kotlin.utils.addToStdlib.ifTrue
  */
 interface ParameterResolver {
     fun tryResolveParameter(name: Name): ExpEmbedding?
-    fun tryResolveReceiver(isExtension: Boolean): ExpEmbedding?
+    fun tryResolveDispatchReceiver(): ExpEmbedding?
+    fun tryResolveExtensionReceiver(labelName: String): ExpEmbedding?
 
-    val sourceName: String?
+    val labelName: String?
     val defaultResolvedReturnTarget: ReturnTarget
 }
 
 fun ParameterResolver.resolveNamedReturnTarget(returnPointName: String): ReturnTarget? =
-    (returnPointName == sourceName).ifTrue { defaultResolvedReturnTarget }
+    (returnPointName == labelName).ifTrue { defaultResolvedReturnTarget }
 
 class RootParameterResolver(
     val ctx: ProgramConversionContext,
     private val signature: FunctionSignature,
-    override val sourceName: String?,
+    override val labelName: String?,
     override val defaultResolvedReturnTarget: ReturnTarget,
 ) : ParameterResolver {
     private val parameters = signature.params.associateBy { it.name }
     override fun tryResolveParameter(name: Name): ExpEmbedding? = parameters[name.embedParameterName()]
-    override fun tryResolveReceiver(isExtension: Boolean) =
-        if (isExtension) signature.extensionReceiver
-        else signature.dispatchReceiver
+    override fun tryResolveDispatchReceiver() = signature.dispatchReceiver
+    override fun tryResolveExtensionReceiver(labelName: String) = (labelName == this.labelName).ifTrue {
+        signature.extensionReceiver
+    }
 }
 
 class InlineParameterResolver(
     private val substitutions: Map<Name, ExpEmbedding>,
-    override val sourceName: String?,
+    override val labelName: String?,
     override val defaultResolvedReturnTarget: ReturnTarget,
 ) : ParameterResolver {
     override fun tryResolveParameter(name: Name): ExpEmbedding? = substitutions[name]
-    override fun tryResolveReceiver(isExtension: Boolean): ExpEmbedding? =
-        if (isExtension) substitutions[ExtraSpecialNames.EXTENSION_THIS]
-        else substitutions[ExtraSpecialNames.DISPATCH_THIS]
+    override fun tryResolveDispatchReceiver() = substitutions[ExtraSpecialNames.DISPATCH_THIS]
+    override fun tryResolveExtensionReceiver(labelName: String) = (labelName == this.labelName).ifTrue {
+        substitutions[ExtraSpecialNames.EXTENSION_THIS]
+    }
 }
\ No newline at end of file
diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ProgramConverter.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ProgramConverter.kt
index 0cceb29a99d3b..e10470da6b1a2 100644
--- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ProgramConverter.kt
+++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ProgramConverter.kt
@@ -241,8 +241,9 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi
     private fun embedFullSignature(symbol: FirFunctionSymbol<*>): FullNamedFunctionSignature {
         val subSignature = object : NamedFunctionSignature, FunctionSignature by embedFunctionSignature(symbol) {
             override val name = symbol.embedName(this@ProgramConverter)
-            override val sourceName: String?
-                get() = super<NamedFunctionSignature>.sourceName
+            override val labelName: String
+                get() = super<NamedFunctionSignature>.labelName
+            override val symbol = symbol
         }
         val constructorParamSymbolsToFields = extractConstructorParamsAsFields(symbol)
         val contractVisitor = ContractDescriptionConversionVisitor(this@ProgramConverter, subSignature)
@@ -371,7 +372,7 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi
     private fun processCallable(symbol: FirFunctionSymbol<*>, signature: FullNamedFunctionSignature): RichCallableEmbedding {
         val body = symbol.fir.body
         return if (symbol.isInline && body != null) {
-            InlineNamedFunction(signature, symbol, body)
+            InlineNamedFunction(signature, body)
         } else {
             // We generate a dummy method header here to ensure all required types are processed already. If we skip this, any types
             // that are used only in contracts cause an error because they are not processed until too late.
@@ -387,7 +388,7 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi
             MethodConverter(
                 this,
                 signature,
-                RootParameterResolver(this, signature, signature.sourceName, returnTarget),
+                RootParameterResolver(this, signature, signature.labelName, returnTarget),
                 scopeDepth = scopeIndexProducer.getFresh(),
             )
         val stmtCtx = StmtConverter(methodCtx)
diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionVisitor.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionVisitor.kt
index 5e8a8582f4fbb..0e2252c1df5a9 100644
--- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionVisitor.kt
+++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionVisitor.kt
@@ -13,6 +13,7 @@ import org.jetbrains.kotlin.fir.expressions.impl.FirElseIfTrueCondition
 import org.jetbrains.kotlin.fir.expressions.impl.FirUnitExpression
 import org.jetbrains.kotlin.fir.references.toResolvedSymbol
 import org.jetbrains.kotlin.fir.symbols.FirBasedSymbol
+import org.jetbrains.kotlin.fir.symbols.impl.FirAnonymousFunctionSymbol
 import org.jetbrains.kotlin.fir.symbols.impl.FirClassSymbol
 import org.jetbrains.kotlin.fir.symbols.impl.FirFunctionSymbol
 import org.jetbrains.kotlin.fir.types.coneType
@@ -319,14 +320,16 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
         // `thisReceiverExpression` has a bound symbol which can be used for lookup
         // for extensions `this`es the bound symbol is the function they originate from
         // for member functions the bound symbol is a class they're defined in
-        // TODO: conduct more thorough lookup based on the name of this symbol as well
-        val isExtensionReceiver = when (thisReceiverExpression.calleeReference.boundSymbol) {
-            is FirClassSymbol<*> -> false
-            is FirFunctionSymbol<*> -> true
+        //
+        // since dispatch receiver can only originate from non-anonymous function we do not specify its name here
+        // as we have only one candidate to resolve it
+        val resolved = when (val symbol = thisReceiverExpression.calleeReference.boundSymbol) {
+            is FirClassSymbol<*> -> data.resolveDispatchReceiver()
+            is FirAnonymousFunctionSymbol -> data.resolveExtensionReceiver(symbol.label!!.name)
+            is FirFunctionSymbol<*> -> data.resolveExtensionReceiver(symbol.name.asString())
             else -> error("Unsupported receiver expression type.")
         }
-        return data.resolveReceiver(isExtensionReceiver)
-            ?: throw IllegalArgumentException("Can't resolve the 'this' receiver since the function does not have one.")
+        return resolved ?: throw IllegalArgumentException("Can't resolve the 'this' receiver since the function does not have one.")
     }
 
     override fun visitTypeOperatorCall(
@@ -355,7 +358,7 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
         data: StmtConversionContext,
     ): ExpEmbedding {
         val function = anonymousFunctionExpression.anonymousFunction
-        return LambdaExp(data.embedFunctionSignature(function.symbol), function, data)
+        return LambdaExp(data.embedFunctionSignature(function.symbol), function, data, function.symbol.label!!.name)
     }
 
     override fun visitTryExpression(tryExpression: FirTryExpression, data: StmtConversionContext): ExpEmbedding {
diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/FullNamedFunctionSignature.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/FullNamedFunctionSignature.kt
index b8d57040eed90..31e7cf39e5219 100644
--- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/FullNamedFunctionSignature.kt
+++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/FullNamedFunctionSignature.kt
@@ -6,6 +6,7 @@
 package org.jetbrains.kotlin.formver.embeddings.callables
 
 import org.jetbrains.kotlin.KtSourceElement
+import org.jetbrains.kotlin.fir.symbols.impl.FirFunctionSymbol
 import org.jetbrains.kotlin.fir.symbols.impl.FirPropertySymbol
 import org.jetbrains.kotlin.formver.asPosition
 import org.jetbrains.kotlin.formver.embeddings.expression.ExpEmbedding
@@ -44,18 +45,22 @@ interface FullNamedFunctionSignature : NamedFunctionSignature {
  */
 abstract class PropertyAccessorFunctionSignature(
     override val name: MangledName,
-    symbol: FirPropertySymbol,
+    propertySymbol: FirPropertySymbol,
 ) : FullNamedFunctionSignature, GenericFunctionSignatureMixin() {
     override fun getPreconditions(returnVariable: VariableEmbedding) = emptyList<ExpEmbedding>()
     override fun getPostconditions(returnVariable: VariableEmbedding) = emptyList<ExpEmbedding>()
     override val dispatchReceiver: VariableEmbedding
         get() = PlaceholderVariableEmbedding(DispatchReceiverName, buildType { nullableAny() })
     override val extensionReceiver = null
-    override val declarationSource: KtSourceElement? = symbol.source
+    override val declarationSource: KtSourceElement? = propertySymbol.source
 }
 
 class GetterFunctionSignature(name: MangledName, symbol: FirPropertySymbol) :
     PropertyAccessorFunctionSignature(name, symbol) {
+    override val symbol: FirFunctionSymbol<*>
+        get() = error {
+            "Getter symbol should not be accessed directly as it is allowed to be null in some cases."
+        }
     override val callableType: FunctionTypeEmbedding = buildFunctionPretype {
         withDispatchReceiver { nullableAny() }
         withReturnType { nullableAny() }
@@ -64,6 +69,10 @@ class GetterFunctionSignature(name: MangledName, symbol: FirPropertySymbol) :
 
 class SetterFunctionSignature(name: MangledName, symbol: FirPropertySymbol) :
     PropertyAccessorFunctionSignature(name, symbol) {
+    override val symbol: FirFunctionSymbol<*>
+        get() = error {
+            "Setter symbol should not be accessed directly as it is allowed to be null in some cases."
+        }
     override val callableType: FunctionTypeEmbedding = buildFunctionPretype {
         withDispatchReceiver { nullableAny() }
         withParam { nullableAny() }
diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/FunctionSignature.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/FunctionSignature.kt
index a0a1363d8f795..43d14cbb6a26e 100644
--- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/FunctionSignature.kt
+++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/FunctionSignature.kt
@@ -19,7 +19,7 @@ interface FunctionSignature {
 
     val params: List<VariableEmbedding>
 
-    val sourceName: String?
+    val labelName: String?
         get() = null
 
     val formalArgs: List<VariableEmbedding>
diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/InlineNamedFunction.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/InlineNamedFunction.kt
index 719033afc1b33..73a4a1a0fac0a 100644
--- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/InlineNamedFunction.kt
+++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/InlineNamedFunction.kt
@@ -14,7 +14,6 @@ import org.jetbrains.kotlin.formver.names.ExtraSpecialNames
 
 class InlineNamedFunction(
     val signature: FullNamedFunctionSignature,
-    val symbol: FirFunctionSymbol<*>,
     val firBody: FirBlock,
 ) : RichCallableEmbedding, FullNamedFunctionSignature by signature {
     override fun insertCall(
@@ -28,7 +27,7 @@ class InlineNamedFunction(
                 add(ExtraSpecialNames.EXTENSION_THIS)
             addAll(symbol.valueParameterSymbols.map { it.name })
         }
-        return ctx.insertInlineFunctionCall(signature, paramNames, args, firBody, signature.sourceName)
+        return ctx.insertInlineFunctionCall(signature, paramNames, args, firBody, signature.labelName)
     }
 
     override fun toViperMethodHeader(): Nothing? = null
diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/NamedFunctionSignature.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/NamedFunctionSignature.kt
index 924a468ec0b51..a8bd3d6007881 100644
--- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/NamedFunctionSignature.kt
+++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/NamedFunctionSignature.kt
@@ -5,20 +5,17 @@
 
 package org.jetbrains.kotlin.formver.embeddings.callables
 
-import org.jetbrains.kotlin.formver.names.FunctionKotlinName
-import org.jetbrains.kotlin.formver.names.ScopedKotlinName
+import org.jetbrains.kotlin.fir.symbols.impl.FirFunctionSymbol
 import org.jetbrains.kotlin.formver.viper.MangledName
 import org.jetbrains.kotlin.formver.viper.ast.*
 
 interface NamedFunctionSignature : FunctionSignature {
     val name: MangledName
-    // TODO: Clean this up; if we want a source name, we should be storing a symbol.
-    override val sourceName: String?
-        get() = when (val signatureName = name) {
-            is FunctionKotlinName -> signatureName.name.asString()
-            is ScopedKotlinName -> (signatureName.name as? FunctionKotlinName)?.name?.asString()
-            else -> null
-        }
+
+    val symbol: FirFunctionSymbol<*>
+
+    override val labelName: String
+        get() = symbol.name.asString()
 }
 
 fun NamedFunctionSignature.toMethodCall(
diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/LambdaExp.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/LambdaExp.kt
index 12e0562287ea0..ed3cc15334605 100644
--- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/LambdaExp.kt
+++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/LambdaExp.kt
@@ -22,6 +22,7 @@ class LambdaExp(
     val signature: FunctionSignature,
     val function: FirAnonymousFunction,
     private val parentCtx: MethodConversionContext,
+    override val labelName: String,
 ) : CallableEmbedding, StoredResultExpEmbedding,
     FunctionSignature by signature {
     override val type: TypeEmbedding
@@ -44,7 +45,7 @@ class LambdaExp(
             receiverParamNames + nonReceiverParamNames,
             args,
             inlineBody,
-            ctx.signature.sourceName,
+            labelName,
             parentCtx,
         )
     }
diff --git a/plugins/formal-verification/testData/diagnostics/verifies/inlining/scoped_receivers.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/verifies/inlining/scoped_receivers.fir.diag.txt
new file mode 100644
index 0000000000000..465637cade06f
--- /dev/null
+++ b/plugins/formal-verification/testData/diagnostics/verifies/inlining/scoped_receivers.fir.diag.txt
@@ -0,0 +1,192 @@
+/scoped_receivers.kt:(407,433): info: Generated Viper text for with_run_extension_labeled:
+field bf$size: Ref
+
+method f$with_run_extension_labeled$TF$NT$Int(this$extension: Ref)
+  returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
+{
+  var anon$13: Ref
+  var anon$14: Ref
+  var ret$1: Ref
+  var anon$15: Ref
+  var anon$16: Ref
+  var ret$3: Ref
+  var anon$0: Ref
+  var anon$17: Ref
+  var ret$4: Ref
+  var anon$1: Ref
+  var anon$18: Ref
+  var anon$19: Ref
+  var ret$5: Ref
+  var anon$2: Ref
+  var anon$20: Ref
+  var ret$6: Ref
+  var anon$3: Ref
+  var anon$21: Ref
+  var ret$7: Ref
+  var anon$4: Ref
+  var anon$22: Ref
+  var ret$8: Ref
+  var anon$5: Ref
+  var anon$23: Ref
+  var ret$9: Ref
+  var anon$6: Ref
+  var anon$24: Ref
+  var anon$25: Ref
+  var ret$10: Ref
+  var anon$7: Ref
+  var anon$26: Ref
+  var ret$11: Ref
+  var anon$8: Ref
+  var anon$27: Ref
+  var anon$28: Ref
+  var ret$12: Ref
+  var anon$29: Ref
+  var anon$30: Ref
+  var ret$14: Ref
+  var anon$9: Ref
+  var anon$31: Ref
+  var ret$15: Ref
+  var anon$10: Ref
+  var anon$32: Ref
+  var anon$33: Ref
+  var ret$16: Ref
+  var anon$11: Ref
+  var anon$34: Ref
+  var ret$17: Ref
+  var anon$12: Ref
+  inhale df$rt$isSubtype(df$rt$typeOf(this$extension), df$rt$nullable(df$rt$intType()))
+  ret$1 := df$rt$boolToRef(this$extension == df$rt$nullValue())
+  goto lbl$ret$1
+  label lbl$ret$1
+  anon$14 := ret$1
+  if (df$rt$boolFromRef(anon$14)) {
+    anon$13 := df$rt$boolToRef(true)
+  } else {
+    var ret$2: Ref
+    ret$2 := sp$notBool(df$rt$boolToRef(this$extension == df$rt$nullValue()))
+    goto lbl$ret$2
+    label lbl$ret$2
+    anon$13 := ret$2
+  }
+  assert df$rt$boolFromRef(anon$13)
+  anon$0 := df$rt$boolToRef(true)
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$0), df$rt$nullable(df$rt$anyType()))
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$0), df$rt$boolType())
+  anon$1 := anon$0
+  anon$2 := df$rt$nullValue()
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$2), df$rt$nullable(df$rt$anyType()))
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$2), df$rt$nullable(df$rt$nothingType()))
+  anon$3 := anon$2
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$3), df$rt$nullable(df$rt$intType()))
+  anon$4 := anon$3
+  ret$7 := df$rt$boolToRef(anon$4 == df$rt$nullValue())
+  goto lbl$ret$7
+  label lbl$ret$7
+  anon$21 := ret$7
+  assert df$rt$boolFromRef(anon$21)
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$3), df$rt$nullable(df$rt$intType()))
+  anon$5 := anon$3
+  ret$8 := df$rt$boolToRef(anon$5 == df$rt$nullValue())
+  goto lbl$ret$8
+  label lbl$ret$8
+  anon$22 := ret$8
+  assert df$rt$boolFromRef(anon$22)
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$3), df$rt$nullable(df$rt$intType()))
+  anon$6 := anon$3
+  ret$9 := df$rt$boolToRef(anon$6 == df$rt$nullValue())
+  goto lbl$ret$9
+  label lbl$ret$9
+  anon$23 := ret$9
+  assert df$rt$boolFromRef(anon$23)
+  label lbl$ret$6
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$6), df$rt$unitType())
+  anon$20 := ret$6
+  ret$5 := anon$20
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$5), df$rt$nullable(df$rt$anyType()))
+  goto lbl$ret$5
+  label lbl$ret$5
+  anon$19 := ret$5
+  anon$18 := anon$19
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$18), df$rt$unitType())
+  assert df$rt$boolFromRef(anon$1)
+  assert df$rt$boolFromRef(anon$1)
+  anon$7 := df$rt$boolToRef(false)
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$7), df$rt$nullable(df$rt$anyType()))
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$7), df$rt$boolType())
+  anon$8 := anon$7
+  assert !df$rt$boolFromRef(anon$8)
+  assert !df$rt$boolFromRef(anon$8)
+  assert df$rt$boolFromRef(anon$1)
+  ret$12 := df$rt$boolToRef(this$extension == df$rt$nullValue())
+  goto lbl$ret$12
+  label lbl$ret$12
+  anon$28 := ret$12
+  if (df$rt$boolFromRef(anon$28)) {
+    anon$27 := df$rt$boolToRef(true)
+  } else {
+    var ret$13: Ref
+    ret$13 := sp$notBool(df$rt$boolToRef(this$extension ==
+      df$rt$nullValue()))
+    goto lbl$ret$13
+    label lbl$ret$13
+    anon$27 := ret$13
+  }
+  assert df$rt$boolFromRef(anon$27)
+  anon$9 := df$rt$boolToRef(false)
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$9), df$rt$nullable(df$rt$anyType()))
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$9), df$rt$boolType())
+  anon$10 := anon$9
+  assert !df$rt$boolFromRef(anon$10)
+  assert !df$rt$boolFromRef(anon$10)
+  assert !df$rt$boolFromRef(anon$8)
+  anon$11 := df$rt$boolToRef(true)
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$11), df$rt$nullable(df$rt$anyType()))
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$11), df$rt$boolType())
+  anon$12 := anon$11
+  assert !df$rt$boolFromRef(anon$10)
+  assert df$rt$boolFromRef(anon$12)
+  assert df$rt$boolFromRef(anon$12)
+  label lbl$ret$17
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$17), df$rt$unitType())
+  anon$34 := ret$17
+  ret$16 := anon$34
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$16), df$rt$nullable(df$rt$anyType()))
+  goto lbl$ret$16
+  label lbl$ret$16
+  anon$33 := ret$16
+  anon$32 := anon$33
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$32), df$rt$unitType())
+  label lbl$ret$15
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$15), df$rt$unitType())
+  anon$31 := ret$15
+  ret$14 := anon$31
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$14), df$rt$nullable(df$rt$anyType()))
+  goto lbl$ret$14
+  label lbl$ret$14
+  anon$30 := ret$14
+  anon$29 := anon$30
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$29), df$rt$unitType())
+  label lbl$ret$11
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$11), df$rt$unitType())
+  anon$26 := ret$11
+  ret$10 := anon$26
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$10), df$rt$nullable(df$rt$anyType()))
+  goto lbl$ret$10
+  label lbl$ret$10
+  anon$25 := ret$10
+  anon$24 := anon$25
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$24), df$rt$unitType())
+  label lbl$ret$4
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$4), df$rt$unitType())
+  anon$17 := ret$4
+  ret$3 := anon$17
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$3), df$rt$nullable(df$rt$anyType()))
+  goto lbl$ret$3
+  label lbl$ret$3
+  anon$16 := ret$3
+  anon$15 := anon$16
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$15), df$rt$unitType())
+  label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
+}
diff --git a/plugins/formal-verification/testData/diagnostics/verifies/inlining/scoped_receivers.kt b/plugins/formal-verification/testData/diagnostics/verifies/inlining/scoped_receivers.kt
new file mode 100644
index 0000000000000..158d5fb4ec0c4
--- /dev/null
+++ b/plugins/formal-verification/testData/diagnostics/verifies/inlining/scoped_receivers.kt
@@ -0,0 +1,51 @@
+// REPLACE_STDLIB_EXTENSIONS
+
+import org.jetbrains.kotlin.formver.plugin.NeverConvert
+import org.jetbrains.kotlin.formver.plugin.AlwaysVerify
+import org.jetbrains.kotlin.formver.plugin.verify
+
+@Suppress("NOTHING_TO_INLINE")
+@NeverConvert
+inline fun Int?.isNull() = this == null
+
+@Suppress("NOTHING_TO_INLINE")
+@NeverConvert
+inline fun Int?.isNotNull() = this != null
+
+@Suppress("LABEL_NAME_CLASH")
+fun Int?.<!VIPER_TEXT!>with_run_extension_labeled<!>() {
+    verify(isNull() || this@with_run_extension_labeled.isNotNull())
+    with(true) {
+        with(null) {
+            verify(
+                isNull(),
+                this.isNull(),
+                this@with.isNull(),
+            )
+        }
+        verify(this, this@with)
+        false.run {
+            verify(
+                !this,
+                !this@run,
+                this@with,
+                this@with_run_extension_labeled.isNull() || isNotNull(),
+            )
+            with(false) {
+                verify(
+                    !this,
+                    !this@with,
+                    !this@run,
+                )
+                with(true) labeled_with@{
+                    verify(
+                        !this@with,
+                        this,
+                        this@labeled_with,
+                    )
+                }
+            }
+        }
+    }
+}
+
diff --git a/plugins/formal-verification/tests-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java b/plugins/formal-verification/tests-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java
index dcc73f6a634a8..f52e313f3aa42 100644
--- a/plugins/formal-verification/tests-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java
+++ b/plugins/formal-verification/tests-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java
@@ -566,6 +566,12 @@ public void testInline_returns() {
         runTest("plugins/formal-verification/testData/diagnostics/verifies/inlining/inline_returns.kt");
       }
 
+      @Test
+      @TestMetadata("scoped_receivers.kt")
+      public void testScoped_receivers() {
+        runTest("plugins/formal-verification/testData/diagnostics/verifies/inlining/scoped_receivers.kt");
+      }
+
       @Test
       @TestMetadata("viper_casts_while_inlining.kt")
       public void testViper_casts_while_inlining() {