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 7e3d1894cadc2..e5e76893e384b 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
@@ -371,20 +371,13 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi
             )
         val stmtCtx = StmtConverter(methodCtx)
         val body = stmtCtx.convert(firBody)
-
-        // In the end we ensure that returned value is of some type even if that type is Unit.
-        // However, for Unit we don't assign the result to any value.
-        // One of the simplest solutions is to do is directly in the beginning of the body.
-        val unitExtendedBody: ExpEmbedding =
-            if (signature.type.returnType != UnitTypeEmbedding) body
-            else blockOf(
-                Assign(stmtCtx.defaultResolvedReturnTarget.variable, UnitLit),
-                body,
-            )
-        val bodyExp = FunctionExp(signature, unitExtendedBody, returnTarget.label)
+        val bodyExp = FunctionExp(signature, body, returnTarget.label)
         val seqnBuilder = SeqnBuilder(declaration.source)
         val linearizer = Linearizer(SharedLinearizationState(anonVarProducer), seqnBuilder, declaration.source)
         bodyExp.toViperUnusedResult(linearizer)
+        // note: we must guarantee somewhere that returned value is Unit
+        // as we may not encounter any `return` statement in the body
+        returnTarget.variable.withIsUnitInvariantIfUnit().toViperUnusedResult(linearizer)
         return FunctionBodyEmbedding(seqnBuilder.block, returnTarget, bodyExp)
     }
 
diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionContext.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionContext.kt
index 7ad39f14d34ec..cd74eeca93994 100644
--- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionContext.kt
+++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionContext.kt
@@ -22,6 +22,7 @@ import org.jetbrains.kotlin.formver.embeddings.expression.*
 import org.jetbrains.kotlin.formver.isCustom
 import org.jetbrains.kotlin.formver.viper.ast.Label
 import org.jetbrains.kotlin.name.Name
+import org.jetbrains.kotlin.utils.addIfNotNull
 import org.jetbrains.kotlin.utils.addToStdlib.ifTrue
 import org.jetbrains.kotlin.utils.filterIsInstanceAnd
 
@@ -131,18 +132,35 @@ fun StmtConversionContext.embedPropertyAccess(accessExpression: FirPropertyAcces
             error("Property access symbol $calleeSymbol has unsupported type.")
     }
 
+
+fun StmtConversionContext.argumentDeclaration(arg: ExpEmbedding, callType: TypeEmbedding): Pair<Declare?, ExpEmbedding> =
+    when (arg.ignoringMetaNodes()) {
+        is LambdaExp -> null to arg
+        else -> {
+            val argWithInvariants = arg.withNewTypeInvariants(callType) {
+                proven = true
+                access = true
+            }
+            // If `argWithInvariants` is `Cast(...(Cast(someVariable))...)` it is fine to use it
+            // since in Viper it will always be translated to `someVariable`.
+            // On other hand, `TypeEmbedding` and invariants in Viper are guaranteed
+            // via previous line.
+            if (argWithInvariants.underlyingVariable != null) null to argWithInvariants
+            else declareAnonVar(callType, argWithInvariants).let {
+                it to it.variable
+            }
+        }
+    }
+
 fun StmtConversionContext.getInlineFunctionCallArgs(
     args: List<ExpEmbedding>,
+    formalArgTypes: List<TypeEmbedding>,
 ): Pair<List<Declare>, List<ExpEmbedding>> {
     val declarations = mutableListOf<Declare>()
-    val storedArgs = args.map { arg ->
-        when (arg.ignoringMetaNodes()) {
-            is VariableEmbedding, is LambdaExp -> arg
-            else -> {
-                val paramVarDecl = declareAnonVar(arg.type, arg)
-                declarations.add(paramVarDecl)
-                paramVarDecl.variable
-            }
+    val storedArgs = args.zip(formalArgTypes).map { (arg, callType) ->
+        argumentDeclaration(arg, callType).let { (declaration, usage) ->
+            declarations.addIfNotNull(declaration)
+            usage
         }
     }
     return Pair(declarations, storedArgs)
@@ -158,7 +176,7 @@ fun StmtConversionContext.insertInlineFunctionCall(
 ): ExpEmbedding {
     // TODO: It seems like it may be possible to avoid creating a local here, but it is not clear how.
     val returnTarget = returnTargetProducer.getFresh(calleeSignature.type.returnType)
-    val (declarations, callArgs) = getInlineFunctionCallArgs(args)
+    val (declarations, callArgs) = getInlineFunctionCallArgs(args, calleeSignature.type.formalArgTypes)
     val subs = paramNames.zip(callArgs).toMap()
     val methodCtxFactory = MethodContextFactory(
         calleeSignature,
@@ -170,7 +188,8 @@ fun StmtConversionContext.insertInlineFunctionCall(
             add(Declare(returnTarget.variable, null))
             addAll(declarations)
             add(FunctionExp(null, convert(body), returnTarget.label))
-            add(returnTarget.variable)
+            // if unit is what we return we might not guarantee it yet
+            add(returnTarget.variable.withIsUnitInvariantIfUnit())
         }
     }
 }
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 e866ce53710ef..2adc55abdf7b5 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
@@ -10,16 +10,19 @@ import org.jetbrains.kotlin.fir.FirElement
 import org.jetbrains.kotlin.fir.declarations.FirProperty
 import org.jetbrains.kotlin.fir.expressions.*
 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.FirFunctionSymbol
 import org.jetbrains.kotlin.fir.types.coneType
+import org.jetbrains.kotlin.fir.types.isUnit
 import org.jetbrains.kotlin.fir.types.resolvedType
 import org.jetbrains.kotlin.fir.visitors.FirVisitor
 import org.jetbrains.kotlin.formver.UnsupportedFeatureBehaviour
 import org.jetbrains.kotlin.formver.embeddings.TypeEmbedding
 import org.jetbrains.kotlin.formver.embeddings.buildType
 import org.jetbrains.kotlin.formver.embeddings.callables.FullNamedFunctionSignature
+import org.jetbrains.kotlin.formver.embeddings.callables.insertCall
 import org.jetbrains.kotlin.formver.embeddings.expression.*
 import org.jetbrains.kotlin.formver.functionCallArguments
 import org.jetbrains.kotlin.text
@@ -48,7 +51,10 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
         returnExpression: FirReturnExpression,
         data: StmtConversionContext,
     ): ExpEmbedding {
-        val expr = data.convert(returnExpression.result)
+        val expr = when (returnExpression.result) {
+            is FirUnitExpression -> UnitLit
+            else -> data.convert(returnExpression.result)
+        }
         // returnTarget is null when it is the implicit return of a lambda
         val returnTargetName = returnExpression.target.labelName
         val target = data.resolveReturnTarget(returnTargetName)
@@ -58,18 +64,25 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
         )
     }
 
+    override fun visitResolvedQualifier(resolvedQualifier: FirResolvedQualifier, data: StmtConversionContext): ExpEmbedding {
+        check(resolvedQualifier.resolvedType.isUnit) {
+            "Only `Unit` is supported among resolved qualifiers currently."
+        }
+        return UnitLit
+    }
+
     override fun visitBlock(block: FirBlock, data: StmtConversionContext): ExpEmbedding =
         block.statements.map(data::convert).toBlock()
 
     override fun visitLiteralExpression(
-        constExpression: FirLiteralExpression,
+        literalExpression: FirLiteralExpression,
         data: StmtConversionContext,
     ): ExpEmbedding =
-        when (constExpression.kind) {
-            ConstantValueKind.Int -> IntLit((constExpression.value as Long).toInt())
-            ConstantValueKind.Boolean -> BooleanLit(constExpression.value as Boolean)
+        when (literalExpression.kind) {
+            ConstantValueKind.Int -> IntLit((literalExpression.value as Long).toInt())
+            ConstantValueKind.Boolean -> BooleanLit(literalExpression.value as Boolean)
             ConstantValueKind.Null -> NullLit
-            else -> handleUnimplementedElement("Constant Expression of type ${constExpression.kind} is not yet implemented.", data)
+            else -> handleUnimplementedElement("Constant Expression of type ${literalExpression.kind} is not yet implemented.", data)
         }
 
     override fun visitIntegerLiteralOperatorCall(
@@ -175,7 +188,11 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
     override fun visitFunctionCall(functionCall: FirFunctionCall, data: StmtConversionContext): ExpEmbedding {
         val symbol = functionCall.toResolvedCallableSymbol()
         val callee = data.embedFunction(symbol as FirFunctionSymbol<*>)
-        return callee.insertCall(functionCall.functionCallArguments.map(data::convert), data)
+        return callee.insertCall(
+            functionCall.functionCallArguments.map(data::convert),
+            data,
+            data.embedType(functionCall.resolvedType),
+        )
     }
 
     override fun visitImplicitInvokeCall(
@@ -184,17 +201,17 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
     ): ExpEmbedding {
         val receiver = implicitInvokeCall.dispatchReceiver as? FirPropertyAccessExpression
             ?: throw NotImplementedError("Implicit invoke calls only support a limited range of receivers at the moment.")
+        val returnType = data.embedType(implicitInvokeCall.resolvedType)
         val receiverSymbol = receiver.calleeReference.toResolvedSymbol<FirBasedSymbol<*>>()!!
         val args = implicitInvokeCall.argumentList.arguments.map(data::convert)
         return when (val exp = data.embedLocalSymbol(receiverSymbol).ignoringMetaNodes()) {
             is LambdaExp -> {
                 // The lambda is already the receiver, so we do not need to convert it.
                 // TODO: do this more uniformly: convert the receiver, see it is a lambda, use insertCall on it.
-                exp.insertCall(args, data)
+                exp.insertCall(args, data, returnType)
             }
             else -> {
-                val retType = data.embedType(implicitInvokeCall.toResolvedCallableSymbol()!!.resolvedReturnType)
-                InvokeFunctionObject(data.convert(receiver), args, retType)
+                InvokeFunctionObject(data.convert(receiver), args, returnType)
             }
         }
     }
diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/CustomAccessors.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/CustomAccessors.kt
index 0ed10fb2c502a..29e5238c5a8f5 100644
--- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/CustomAccessors.kt
+++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/CustomAccessors.kt
@@ -7,13 +7,14 @@ package org.jetbrains.kotlin.formver.embeddings
 
 import org.jetbrains.kotlin.formver.conversion.StmtConversionContext
 import org.jetbrains.kotlin.formver.embeddings.callables.CallableEmbedding
+import org.jetbrains.kotlin.formver.embeddings.callables.insertCall
 import org.jetbrains.kotlin.formver.embeddings.expression.ExpEmbedding
 
 class CustomGetter(val getterMethod: CallableEmbedding) : GetterEmbedding {
     override fun getValue(
         receiver: ExpEmbedding,
         ctx: StmtConversionContext,
-    ): ExpEmbedding = getterMethod.insertCall(listOf(receiver), ctx)
+    ): ExpEmbedding = getterMethod.insertCall(listOf(receiver), ctx, getterMethod.type.returnType)
 }
 
 class CustomSetter(val setterMethod: CallableEmbedding) : SetterEmbedding {
@@ -21,5 +22,5 @@ class CustomSetter(val setterMethod: CallableEmbedding) : SetterEmbedding {
         receiver: ExpEmbedding,
         value: ExpEmbedding,
         ctx: StmtConversionContext,
-    ): ExpEmbedding = setterMethod.insertCall(listOf(receiver, value), ctx)
+    ): ExpEmbedding = setterMethod.insertCall(listOf(receiver, value), ctx, setterMethod.type.returnType)
 }
diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/TypeBuilder.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/TypeBuilder.kt
index ce0cc255a1027..c4e25bf77d9c8 100644
--- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/TypeBuilder.kt
+++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/TypeBuilder.kt
@@ -39,6 +39,8 @@ fun TypeBuilder.nullableAny(): AnyPretypeBuilder {
 
 fun buildType(init: TypeBuilder.() -> PretypeBuilder): TypeEmbedding = TypeBuilder().complete(init)
 
+fun TypeEmbedding.equalToType(init: TypeBuilder.() -> PretypeBuilder) = equals(buildType { init() })
+
 fun buildFunctionType(init: FunctionPretypeBuilder.() -> Unit): FunctionTypeEmbedding =
     buildType { function { init() } } as FunctionTypeEmbedding
 
diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/TypeEmbedding.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/TypeEmbedding.kt
index a07a4634876fb..ab3ea58bb6b60 100644
--- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/TypeEmbedding.kt
+++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/TypeEmbedding.kt
@@ -12,6 +12,7 @@ import org.jetbrains.kotlin.formver.names.NameMatcher
 import org.jetbrains.kotlin.formver.viper.MangledName
 import org.jetbrains.kotlin.formver.viper.ast.Exp
 import org.jetbrains.kotlin.formver.viper.mangled
+import org.jetbrains.kotlin.utils.addToStdlib.ifFalse
 
 /**
  * Represents our representation of a Kotlin type.
@@ -183,4 +184,3 @@ val TypeEmbedding.isCollectionInheritor
     get() = isInheritorOfCollectionTypeNamed("Collection")
 
 fun TypeEmbedding.subTypeInvariant() = SubTypeInvariantEmbedding(this)
-
diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/CallableEmbedding.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/CallableEmbedding.kt
index 858b7fa9aa5b5..714e4d71f4130 100644
--- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/CallableEmbedding.kt
+++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/CallableEmbedding.kt
@@ -7,7 +7,9 @@ package org.jetbrains.kotlin.formver.embeddings.callables
 
 import org.jetbrains.kotlin.formver.conversion.StmtConversionContext
 import org.jetbrains.kotlin.formver.embeddings.FunctionTypeEmbedding
+import org.jetbrains.kotlin.formver.embeddings.TypeEmbedding
 import org.jetbrains.kotlin.formver.embeddings.expression.ExpEmbedding
+import org.jetbrains.kotlin.formver.embeddings.expression.withNewTypeInvariants
 
 /**
  * Kotlin entity that can be called.
@@ -16,3 +18,9 @@ interface CallableEmbedding {
     val type: FunctionTypeEmbedding
     fun insertCall(args: List<ExpEmbedding>, ctx: StmtConversionContext): ExpEmbedding
 }
+
+fun CallableEmbedding.insertCall(args: List<ExpEmbedding>, ctx: StmtConversionContext, actualReturnType: TypeEmbedding) =
+    insertCall(args, ctx).withNewTypeInvariants(actualReturnType) {
+        access = true
+        proven = true
+    }
\ No newline at end of file
diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/TypeOp.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/TypeOp.kt
index 8f0ad5600188b..7b95bbebeccdb 100644
--- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/TypeOp.kt
+++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/TypeOp.kt
@@ -160,6 +160,10 @@ inline fun ExpEmbedding.withInvariants(block: InhaleInvariantsBuilder.() -> Unit
     return builder.complete()
 }
 
+fun ExpEmbedding.withIsUnitInvariantIfUnit() = withInvariants {
+    proven = type.equalToType { unit() }
+}
+
 inline fun ExpEmbedding.withNewTypeInvariants(newType: TypeEmbedding, block: InhaleInvariantsBuilder.() -> Unit) =
     if (this.type == newType) this else withType(newType).withInvariants(block)
 
diff --git a/plugins/formal-verification/testData/diagnostics/bad_contracts/cond_effects.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/bad_contracts/cond_effects.fir.diag.txt
index 156b6f6908403..e987b053946c5 100644
--- a/plugins/formal-verification/testData/diagnostics/bad_contracts/cond_effects.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/bad_contracts/cond_effects.fir.diag.txt
@@ -5,8 +5,8 @@ method f$compoundConditionalEffect$TF$T$Boolean(p$b: Ref)
   ensures true ==> df$rt$boolFromRef(p$b) && false
 {
   inhale df$rt$isSubtype(df$rt$typeOf(p$b), df$rt$boolType())
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /cond_effects.kt:(190,220): warning: Cannot verify that if the function returns then (b && false).
diff --git a/plugins/formal-verification/testData/diagnostics/bad_contracts/is_type_contract.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/bad_contracts/is_type_contract.fir.diag.txt
index 5438f4ed2acf4..735ee96e51bed 100644
--- a/plugins/formal-verification/testData/diagnostics/bad_contracts/is_type_contract.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/bad_contracts/is_type_contract.fir.diag.txt
@@ -22,8 +22,8 @@ method f$nullableNotNonNullable$TF$Int(p$x: Ref) returns (ret$0: Ref)
   ensures true ==> df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$intType())
 {
   inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$nullable(df$rt$intType()))
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /is_type_contract.kt:(376,404): warning: Cannot verify that if the function returns then x is Int.
diff --git a/plugins/formal-verification/testData/diagnostics/bad_contracts/list.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/bad_contracts/list.fir.diag.txt
index 97aa94fa827ca..3f8fc620e8292 100644
--- a/plugins/formal-verification/testData/diagnostics/bad_contracts/list.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/bad_contracts/list.fir.diag.txt
@@ -6,11 +6,11 @@ method f$empty_list_expr_get$TF$() returns (ret$0: Ref)
 {
   var l0$s: Ref
   var anon$0: Ref
-  ret$0 := df$rt$unitValue()
   anon$0 := f$pkg$kotlin_collections$emptyList$TF$()
   l0$s := f$pkg$kotlin_collections$c$List$get$TF$T$c$pkg$kotlin_collections$List$T$Int(anon$0,
     df$rt$intToRef(0))
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method f$pkg$kotlin_collections$c$List$get$TF$T$c$pkg$kotlin_collections$List$T$Int(this: Ref,
@@ -45,11 +45,11 @@ method f$empty_list_get$TF$() returns (ret$0: Ref)
 {
   var l0$myList: Ref
   var l0$s: Ref
-  ret$0 := df$rt$unitValue()
   l0$myList := f$pkg$kotlin_collections$emptyList$TF$()
   l0$s := f$pkg$kotlin_collections$c$List$get$TF$T$c$pkg$kotlin_collections$List$T$Int(l0$myList,
     df$rt$intToRef(0))
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method f$pkg$kotlin_collections$c$List$get$TF$T$c$pkg$kotlin_collections$List$T$Int(this: Ref,
@@ -129,12 +129,12 @@ method f$add_get$TF$T$c$pkg$kotlin_collections$MutableList(p$l: Ref)
   var l0$n: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$l), df$rt$T$c$pkg$kotlin_collections$MutableList())
   inhale acc(p$pkg$kotlin_collections$c$MutableList$shared(p$l), wildcard)
-  ret$0 := df$rt$unitValue()
   anon$0 := f$pkg$kotlin_collections$c$MutableList$add$TF$T$c$pkg$kotlin_collections$MutableList$T$Int(p$l,
     df$rt$intToRef(1))
   l0$n := f$pkg$kotlin_collections$c$MutableList$get$TF$T$c$pkg$kotlin_collections$MutableList$T$Int(p$l,
     df$rt$intToRef(1))
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method f$pkg$kotlin_collections$c$MutableList$add$TF$T$c$pkg$kotlin_collections$MutableList$T$Int(this: Ref,
@@ -173,11 +173,11 @@ method f$empty_list_sub$TF$() returns (ret$0: Ref)
 {
   var l0$l: Ref
   var anon$0: Ref
-  ret$0 := df$rt$unitValue()
   anon$0 := f$pkg$kotlin_collections$emptyList$TF$()
   l0$l := f$pkg$kotlin_collections$c$List$subList$TF$T$c$pkg$kotlin_collections$List$T$Int$T$Int(anon$0,
     df$rt$intToRef(0), df$rt$intToRef(1))
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method f$pkg$kotlin_collections$c$List$subList$TF$T$c$pkg$kotlin_collections$List$T$Int$T$Int(this: Ref,
@@ -218,11 +218,11 @@ method f$empty_list_sub_negative$TF$() returns (ret$0: Ref)
 {
   var l0$l: Ref
   var anon$0: Ref
-  ret$0 := df$rt$unitValue()
   anon$0 := f$pkg$kotlin_collections$emptyList$TF$()
   l0$l := f$pkg$kotlin_collections$c$List$subList$TF$T$c$pkg$kotlin_collections$List$T$Int$T$Int(anon$0,
     df$rt$intToRef(-1), df$rt$intToRef(1))
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method f$pkg$kotlin_collections$c$List$subList$TF$T$c$pkg$kotlin_collections$List$T$Int$T$Int(this: Ref,
diff --git a/plugins/formal-verification/testData/diagnostics/bad_contracts/viper_verify.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/bad_contracts/viper_verify.fir.diag.txt
index e1e8a15cf3768..2abe319c1ec75 100644
--- a/plugins/formal-verification/testData/diagnostics/bad_contracts/viper_verify.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/bad_contracts/viper_verify.fir.diag.txt
@@ -2,9 +2,9 @@
 method f$verify_false$TF$() returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
-  ret$0 := df$rt$unitValue()
   assert false
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /viper_verify.kt:(153,158): warning: Viper verification error: Assert might fail. Assertion false might not hold.
@@ -14,13 +14,13 @@ method f$verify_compound$TF$() returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   var anon$0: Ref
-  ret$0 := df$rt$unitValue()
   if (true) {
     anon$0 := df$rt$boolToRef(false)
   } else {
     anon$0 := df$rt$boolToRef(false)}
   assert df$rt$boolFromRef(anon$0)
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /viper_verify.kt:(212,225): warning: Viper verification error: Assert might fail. Assertion df$rt$boolFromRef(anon$0) might not hold.
diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/custom_list.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/good_contracts/custom_list.fir.diag.txt
index 23ab7e54609aa..c7f53e968d445 100644
--- a/plugins/formal-verification/testData/diagnostics/good_contracts/custom_list.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/good_contracts/custom_list.fir.diag.txt
@@ -70,7 +70,6 @@ method f$test$TF$T$Int(p$n: Ref) returns (ret$0: Ref)
   var l0$customList: Ref
   var anon$0: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$n), df$rt$intType())
-  ret$0 := df$rt$unitValue()
   l0$customList := con$c$CustomList$T$Int$T$Int(p$n, df$rt$intToRef(0))
   anon$0 := f$c$CustomList$isEmpty$TF$T$c$CustomList(l0$customList)
   if (!df$rt$boolFromRef(anon$0)) {
@@ -84,4 +83,5 @@ method f$test$TF$T$Int(p$n: Ref) returns (ret$0: Ref)
     anon$3 := f$c$CustomList$get$TF$T$c$CustomList$T$Int(l0$customList, df$rt$intToRef(0))
   }
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/custom_run_functions.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/good_contracts/custom_run_functions.fir.diag.txt
index 9afc5476b0f69..41873bf0a8926 100644
--- a/plugins/formal-verification/testData/diagnostics/good_contracts/custom_run_functions.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/good_contracts/custom_run_functions.fir.diag.txt
@@ -7,143 +7,171 @@ method f$useRun$TF$() returns (ret$0: Ref)
   var l0$two: Ref
   var l0$three: Ref
   var l0$genericResult: Ref
-  var anon$9: Ref
-  var ret$1: Ref
   var anon$10: Ref
-  var ret$2: Ref
   var anon$11: Ref
-  var ret$3: Ref
+  var ret$1: Ref
   var anon$12: Ref
-  var ret$4: Ref
+  var ret$2: Ref
   var anon$13: Ref
-  var ret$5: Ref
   var anon$14: Ref
+  var ret$3: Ref
+  var anon$15: Ref
+  var ret$4: Ref
+  var anon$16: Ref
+  var anon$17: Ref
+  var ret$5: Ref
+  var anon$18: Ref
   var ret$6: Ref
   var l0$capturedResult: Ref
-  var anon$15: Ref
+  var anon$19: Ref
+  var anon$20: Ref
   var ret$7: Ref
-  var anon$16: Ref
+  var anon$21: Ref
   var ret$8: Ref
-  var anon$17: Ref
+  var anon$22: Ref
+  var anon$23: Ref
   var ret$9: Ref
-  var anon$18: Ref
+  var anon$24: Ref
   var ret$10: Ref
-  var anon$19: Ref
+  var anon$25: Ref
+  var anon$26: Ref
   var ret$11: Ref
-  var anon$20: Ref
+  var anon$27: Ref
   var ret$12: Ref
   var l0$intResult: Ref
-  var anon$21: Ref
+  var anon$28: Ref
   var ret$13: Ref
   var ret$14: Ref
-  var anon$22: Ref
+  var anon$29: Ref
   var ret$15: Ref
   var ret$16: Ref
-  var anon$23: Ref
+  var anon$30: Ref
   var ret$17: Ref
   var ret$18: Ref
   var l0$doubleIntRunResult: Ref
-  var anon$24: Ref
+  var anon$31: Ref
   var ret$19: Ref
   var anon$0: Ref
   var ret$21: Ref
   var anon$1: Ref
   var ret$20: Ref
   var l0$genericReceiverResult: Ref
-  var anon$25: Ref
-  var ret$22: Ref
-  var anon$2: Ref
-  var anon$26: Ref
-  var ret$23: Ref
-  var anon$27: Ref
-  var anon$28: Ref
-  var anon$29: Ref
-  var anon$30: Ref
-  var anon$31: Ref
   var anon$32: Ref
   var anon$33: Ref
+  var ret$22: Ref
+  var anon$2: Ref
   var anon$34: Ref
+  var ret$23: Ref
+  var anon$3: Ref
   var anon$35: Ref
   var anon$36: Ref
+  var anon$37: Ref
+  var anon$38: Ref
+  var anon$39: Ref
+  var anon$40: Ref
+  var anon$41: Ref
+  var anon$42: Ref
+  var anon$43: Ref
+  var anon$44: Ref
   l0$one := df$rt$intToRef(1)
   l0$two := df$rt$intToRef(2)
   l0$three := df$rt$intToRef(3)
   ret$2 := df$rt$intToRef(1)
   goto lbl$ret$2
   label lbl$ret$2
-  anon$10 := ret$2
-  ret$1 := anon$10
+  anon$12 := ret$2
+  ret$1 := anon$12
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$1), df$rt$nullable(df$rt$anyType()))
   goto lbl$ret$1
   label lbl$ret$1
-  anon$9 := ret$1
+  anon$11 := ret$1
+  anon$10 := anon$11
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$10), df$rt$intType())
   ret$4 := df$rt$intToRef(2)
   goto lbl$ret$4
   label lbl$ret$4
-  anon$12 := ret$4
-  ret$3 := anon$12
+  anon$15 := ret$4
+  ret$3 := anon$15
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$3), df$rt$nullable(df$rt$anyType()))
   goto lbl$ret$3
   label lbl$ret$3
-  anon$11 := ret$3
+  anon$14 := ret$3
+  anon$13 := anon$14
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$13), df$rt$intType())
   ret$6 := df$rt$intToRef(3)
   goto lbl$ret$6
   label lbl$ret$6
-  anon$14 := ret$6
-  ret$5 := anon$14
+  anon$18 := ret$6
+  ret$5 := anon$18
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$5), df$rt$nullable(df$rt$anyType()))
   goto lbl$ret$5
   label lbl$ret$5
-  anon$13 := ret$5
-  l0$genericResult := df$rt$boolToRef(sp$plusInts(anon$9, anon$11) ==
-    anon$13)
+  anon$17 := ret$5
+  anon$16 := anon$17
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$16), df$rt$intType())
+  l0$genericResult := df$rt$boolToRef(df$rt$intFromRef(anon$10) +
+    df$rt$intFromRef(anon$13) ==
+    df$rt$intFromRef(anon$16))
   ret$8 := df$rt$intToRef(1)
   goto lbl$ret$8
   label lbl$ret$8
-  anon$16 := ret$8
-  ret$7 := anon$16
+  anon$21 := ret$8
+  ret$7 := anon$21
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$7), df$rt$nullable(df$rt$anyType()))
   goto lbl$ret$7
   label lbl$ret$7
-  anon$15 := ret$7
+  anon$20 := ret$7
+  anon$19 := anon$20
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$19), df$rt$intType())
   ret$10 := df$rt$intToRef(2)
   goto lbl$ret$10
   label lbl$ret$10
-  anon$18 := ret$10
-  ret$9 := anon$18
+  anon$24 := ret$10
+  ret$9 := anon$24
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$9), df$rt$nullable(df$rt$anyType()))
   goto lbl$ret$9
   label lbl$ret$9
-  anon$17 := ret$9
+  anon$23 := ret$9
+  anon$22 := anon$23
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$22), df$rt$intType())
   ret$12 := df$rt$intToRef(3)
   goto lbl$ret$12
   label lbl$ret$12
-  anon$20 := ret$12
-  ret$11 := anon$20
+  anon$27 := ret$12
+  ret$11 := anon$27
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$11), df$rt$nullable(df$rt$anyType()))
   goto lbl$ret$11
   label lbl$ret$11
-  anon$19 := ret$11
-  l0$capturedResult := df$rt$boolToRef(sp$plusInts(anon$15, anon$17) ==
-    anon$19)
+  anon$26 := ret$11
+  anon$25 := anon$26
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$25), df$rt$intType())
+  l0$capturedResult := df$rt$boolToRef(df$rt$intFromRef(anon$19) +
+    df$rt$intFromRef(anon$22) ==
+    df$rt$intFromRef(anon$25))
   ret$14 := df$rt$intToRef(1)
   goto lbl$ret$14
   label lbl$ret$14
   ret$13 := ret$14
   goto lbl$ret$13
   label lbl$ret$13
-  anon$21 := ret$13
+  anon$28 := ret$13
   ret$16 := df$rt$intToRef(2)
   goto lbl$ret$16
   label lbl$ret$16
   ret$15 := ret$16
   goto lbl$ret$15
   label lbl$ret$15
-  anon$22 := ret$15
+  anon$29 := ret$15
   ret$18 := df$rt$intToRef(3)
   goto lbl$ret$18
   label lbl$ret$18
   ret$17 := ret$18
   goto lbl$ret$17
   label lbl$ret$17
-  anon$23 := ret$17
-  l0$intResult := df$rt$boolToRef(df$rt$intFromRef(anon$21) +
-    df$rt$intFromRef(anon$22) ==
-    df$rt$intFromRef(anon$23))
+  anon$30 := ret$17
+  l0$intResult := df$rt$boolToRef(df$rt$intFromRef(anon$28) +
+    df$rt$intFromRef(anon$29) ==
+    df$rt$intFromRef(anon$30))
   anon$0 := df$rt$intToRef(1)
   ret$20 := sp$plusInts(anon$0, df$rt$intToRef(1))
   goto lbl$ret$20
@@ -155,27 +183,34 @@ method f$useRun$TF$() returns (ret$0: Ref)
   ret$19 := ret$21
   goto lbl$ret$19
   label lbl$ret$19
-  anon$24 := ret$19
-  l0$doubleIntRunResult := df$rt$boolToRef(df$rt$intFromRef(anon$24) == 3)
+  anon$31 := ret$19
+  l0$doubleIntRunResult := df$rt$boolToRef(df$rt$intFromRef(anon$31) == 3)
   anon$2 := df$rt$intToRef(1)
-  ret$23 := sp$plusInts(anon$2, df$rt$intToRef(2))
+  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$intType())
+  anon$3 := anon$2
+  ret$23 := sp$plusInts(anon$3, df$rt$intToRef(2))
   goto lbl$ret$23
   label lbl$ret$23
-  anon$26 := ret$23
-  ret$22 := anon$26
+  anon$34 := ret$23
+  ret$22 := anon$34
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$22), df$rt$nullable(df$rt$anyType()))
   goto lbl$ret$22
   label lbl$ret$22
-  anon$25 := ret$22
-  l0$genericReceiverResult := df$rt$boolToRef(anon$25 == df$rt$intToRef(3))
+  anon$33 := ret$22
+  anon$32 := anon$33
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$32), df$rt$intType())
+  l0$genericReceiverResult := df$rt$boolToRef(df$rt$intFromRef(anon$32) ==
+    3)
   if (df$rt$boolFromRef(l0$intResult)) {
-    anon$36 := l0$genericResult
+    anon$44 := l0$genericResult
   } else {
-    anon$36 := df$rt$boolToRef(false)}
-  if (df$rt$boolFromRef(anon$36)) {
-    anon$35 := l0$capturedResult
+    anon$44 := df$rt$boolToRef(false)}
+  if (df$rt$boolFromRef(anon$44)) {
+    anon$43 := l0$capturedResult
   } else {
-    anon$35 := df$rt$boolToRef(false)}
-  if (df$rt$boolFromRef(anon$35)) {
+    anon$43 := df$rt$boolToRef(false)}
+  if (df$rt$boolFromRef(anon$43)) {
     var ret$24: Ref
     var l24$result: Ref
     var ret$25: Ref
@@ -186,11 +221,11 @@ method f$useRun$TF$() returns (ret$0: Ref)
     ret$24 := df$rt$boolToRef(df$rt$intFromRef(l24$result) == 3)
     goto lbl$ret$24
     label lbl$ret$24
-    anon$34 := ret$24
+    anon$42 := ret$24
   } else {
-    anon$34 := df$rt$boolToRef(false)}
-  if (df$rt$boolFromRef(anon$34)) {
-    var anon$37: Ref
+    anon$42 := df$rt$boolToRef(false)}
+  if (df$rt$boolFromRef(anon$42)) {
+    var anon$45: Ref
     var ret$26: Ref
     var l26$result: Ref
     var ret$27: Ref
@@ -201,103 +236,103 @@ method f$useRun$TF$() returns (ret$0: Ref)
     ret$26 := df$rt$boolToRef(df$rt$intFromRef(l26$result) == 3)
     goto lbl$ret$26
     label lbl$ret$26
-    anon$37 := ret$26
-    anon$33 := sp$notBool(anon$37)
+    anon$45 := ret$26
+    anon$41 := sp$notBool(anon$45)
   } else {
-    anon$33 := df$rt$boolToRef(false)}
-  if (df$rt$boolFromRef(anon$33)) {
+    anon$41 := df$rt$boolToRef(false)}
+  if (df$rt$boolFromRef(anon$41)) {
     var ret$28: Ref
     var l28$result: Ref
     var ret$29: Ref
-    var anon$3: Ref
-    anon$3 := df$rt$intToRef(1)
-    ret$29 := sp$plusInts(anon$3, df$rt$intToRef(2))
+    var anon$4: Ref
+    anon$4 := df$rt$intToRef(1)
+    ret$29 := sp$plusInts(anon$4, df$rt$intToRef(2))
     goto lbl$ret$29
     label lbl$ret$29
     l28$result := ret$29
     ret$28 := df$rt$boolToRef(df$rt$intFromRef(l28$result) == 3)
     goto lbl$ret$28
     label lbl$ret$28
-    anon$32 := ret$28
+    anon$40 := ret$28
   } else {
-    anon$32 := df$rt$boolToRef(false)}
-  if (df$rt$boolFromRef(anon$32)) {
-    var anon$38: Ref
+    anon$40 := df$rt$boolToRef(false)}
+  if (df$rt$boolFromRef(anon$40)) {
+    var anon$46: Ref
     var ret$30: Ref
     var l30$result: Ref
     var ret$31: Ref
-    var anon$4: Ref
-    anon$4 := df$rt$intToRef(1)
-    ret$31 := anon$4
+    var anon$5: Ref
+    anon$5 := df$rt$intToRef(1)
+    ret$31 := anon$5
     goto lbl$ret$31
     label lbl$ret$31
     l30$result := ret$31
     ret$30 := df$rt$boolToRef(df$rt$intFromRef(l30$result) == 3)
     goto lbl$ret$30
     label lbl$ret$30
-    anon$38 := ret$30
-    anon$31 := sp$notBool(anon$38)
+    anon$46 := ret$30
+    anon$39 := sp$notBool(anon$46)
   } else {
-    anon$31 := df$rt$boolToRef(false)}
-  if (df$rt$boolFromRef(anon$31)) {
+    anon$39 := df$rt$boolToRef(false)}
+  if (df$rt$boolFromRef(anon$39)) {
     var ret$32: Ref
     var l32$result: Ref
     var ret$33: Ref
-    var anon$5: Ref
-    anon$5 := df$rt$intToRef(1)
-    ret$33 := sp$plusInts(anon$5, df$rt$intToRef(2))
+    var anon$6: Ref
+    anon$6 := df$rt$intToRef(1)
+    ret$33 := sp$plusInts(anon$6, df$rt$intToRef(2))
     goto lbl$ret$33
     label lbl$ret$33
     l32$result := ret$33
     ret$32 := df$rt$boolToRef(df$rt$intFromRef(l32$result) == 3)
     goto lbl$ret$32
     label lbl$ret$32
-    anon$30 := ret$32
+    anon$38 := ret$32
   } else {
-    anon$30 := df$rt$boolToRef(false)}
-  if (df$rt$boolFromRef(anon$30)) {
+    anon$38 := df$rt$boolToRef(false)}
+  if (df$rt$boolFromRef(anon$38)) {
     var ret$34: Ref
     var l34$result: Ref
     var ret$35: Ref
-    var anon$6: Ref
-    anon$6 := df$rt$intToRef(1)
-    ret$35 := sp$plusInts(anon$6, df$rt$intToRef(2))
+    var anon$7: Ref
+    anon$7 := df$rt$intToRef(1)
+    ret$35 := sp$plusInts(anon$7, df$rt$intToRef(2))
     goto lbl$ret$35
     label lbl$ret$35
     l34$result := ret$35
     ret$34 := df$rt$boolToRef(df$rt$intFromRef(l34$result) == 3)
     goto lbl$ret$34
     label lbl$ret$34
-    anon$29 := ret$34
+    anon$37 := ret$34
   } else {
-    anon$29 := df$rt$boolToRef(false)}
-  if (df$rt$boolFromRef(anon$29)) {
+    anon$37 := df$rt$boolToRef(false)}
+  if (df$rt$boolFromRef(anon$37)) {
     var ret$36: Ref
     var l36$result: Ref
     var ret$38: Ref
-    var anon$8: Ref
+    var anon$9: Ref
     var ret$37: Ref
-    var anon$7: Ref
-    anon$7 := df$rt$intToRef(1)
-    ret$37 := sp$plusInts(anon$7, df$rt$intToRef(1))
+    var anon$8: Ref
+    anon$8 := df$rt$intToRef(1)
+    ret$37 := sp$plusInts(anon$8, df$rt$intToRef(1))
     goto lbl$ret$37
     label lbl$ret$37
-    anon$8 := ret$37
-    ret$38 := sp$plusInts(anon$8, df$rt$intToRef(1))
+    anon$9 := ret$37
+    ret$38 := sp$plusInts(anon$9, df$rt$intToRef(1))
     goto lbl$ret$38
     label lbl$ret$38
     l36$result := ret$38
     ret$36 := df$rt$boolToRef(df$rt$intFromRef(l36$result) == 3)
     goto lbl$ret$36
     label lbl$ret$36
-    anon$28 := ret$36
+    anon$36 := ret$36
   } else {
-    anon$28 := df$rt$boolToRef(false)}
-  if (df$rt$boolFromRef(anon$28)) {
-    anon$27 := l0$doubleIntRunResult
+    anon$36 := df$rt$boolToRef(false)}
+  if (df$rt$boolFromRef(anon$36)) {
+    anon$35 := l0$doubleIntRunResult
   } else {
-    anon$27 := df$rt$boolToRef(false)}
-  if (df$rt$boolFromRef(anon$27)) {
+    anon$35 := df$rt$boolToRef(false)}
+  if (df$rt$boolFromRef(anon$35)) {
     ret$0 := l0$genericReceiverResult
   } else {
     ret$0 := df$rt$boolToRef(false)}
@@ -311,31 +346,38 @@ method f$complexScenario$TF$T$Boolean(p$arg: Ref) returns (ret$0: Ref)
   ensures df$rt$boolFromRef(ret$0) == true ==> df$rt$boolFromRef(p$arg)
   ensures df$rt$boolFromRef(ret$0) == false ==> !df$rt$boolFromRef(p$arg)
 {
-  var anon$5: Ref
+  var anon$11: Ref
+  var anon$12: Ref
   var ret$1: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$arg), df$rt$boolType())
   if (df$rt$boolFromRef(p$arg)) {
-    var anon$6: Ref
+    var anon$13: Ref
     var ret$2: Ref
-    var anon$7: Ref
+    var anon$14: Ref
     var ret$3: Ref
     var l5$result: Ref
     var ret$4: Ref
     var anon$0: Ref
-    var anon$8: Ref
+    var anon$15: Ref
     var ret$5: Ref
-    var anon$9: Ref
+    var anon$1: Ref
+    var anon$16: Ref
     var ret$6: Ref
+    var anon$2: Ref
     var ret$7: Ref
     var ret$9: Ref
-    var anon$1: Ref
+    var anon$3: Ref
     var ret$8: Ref
     anon$0 := df$rt$intToRef(1)
-    ret$8 := sp$plusInts(anon$0, df$rt$intToRef(1))
+    inhale df$rt$isSubtype(df$rt$typeOf(anon$0), df$rt$nullable(df$rt$anyType()))
+    anon$1 := anon$0
+    inhale df$rt$isSubtype(df$rt$typeOf(anon$1), df$rt$intType())
+    anon$2 := anon$1
+    ret$8 := sp$plusInts(anon$2, df$rt$intToRef(1))
     goto lbl$ret$8
     label lbl$ret$8
-    anon$1 := ret$8
-    ret$9 := sp$plusInts(anon$1, df$rt$intToRef(1))
+    anon$3 := ret$8
+    ret$9 := sp$plusInts(anon$3, df$rt$intToRef(1))
     goto lbl$ret$9
     label lbl$ret$9
     ret$7 := ret$9
@@ -344,85 +386,110 @@ method f$complexScenario$TF$T$Boolean(p$arg: Ref) returns (ret$0: Ref)
     ret$6 := ret$7
     goto lbl$ret$6
     label lbl$ret$6
-    anon$9 := ret$6
-    ret$5 := anon$9
+    anon$16 := ret$6
+    ret$5 := anon$16
+    inhale df$rt$isSubtype(df$rt$typeOf(ret$5), df$rt$nullable(df$rt$anyType()))
     goto lbl$ret$5
     label lbl$ret$5
-    anon$8 := ret$5
-    ret$4 := anon$8
+    anon$15 := ret$5
+    ret$4 := anon$15
+    inhale df$rt$isSubtype(df$rt$typeOf(ret$4), df$rt$intType())
     goto lbl$ret$4
     label lbl$ret$4
     l5$result := ret$4
     ret$3 := df$rt$boolToRef(df$rt$intFromRef(l5$result) == 3)
     goto lbl$ret$3
     label lbl$ret$3
-    anon$7 := ret$3
-    ret$2 := anon$7
+    anon$14 := ret$3
+    ret$2 := anon$14
     goto lbl$ret$2
     label lbl$ret$2
-    anon$6 := ret$2
-    ret$1 := anon$6
+    anon$13 := ret$2
+    ret$1 := anon$13
+    inhale df$rt$isSubtype(df$rt$typeOf(ret$1), df$rt$nullable(df$rt$anyType()))
   } else {
-    var anon$10: Ref
-    anon$10 := df$rt$nullValue()
-    ret$1 := anon$10
+    var anon$17: Ref
+    anon$17 := df$rt$nullValue()
+    ret$1 := anon$17
   }
   goto lbl$ret$1
   label lbl$ret$1
-  anon$5 := ret$1
-  if (anon$5 != df$rt$nullValue()) {
-    ret$0 := anon$5
+  anon$12 := ret$1
+  anon$11 := anon$12
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$11), df$rt$nullable(df$rt$boolType()))
+  if (anon$11 != df$rt$nullValue()) {
+    ret$0 := anon$11
   } else {
-    var anon$11: Ref
+    var anon$18: Ref
     var ret$10: Ref
-    var anon$12: Ref
+    var anon$19: Ref
     var ret$11: Ref
     var ret$12: Ref
     var l15$result: Ref
     var ret$13: Ref
-    var anon$2: Ref
-    var anon$13: Ref
+    var anon$4: Ref
+    var anon$20: Ref
     var ret$14: Ref
-    var anon$14: Ref
+    var anon$5: Ref
+    var anon$21: Ref
     var ret$15: Ref
-    var anon$15: Ref
+    var anon$6: Ref
+    var anon$22: Ref
     var ret$16: Ref
-    var anon$3: Ref
-    var anon$16: Ref
+    var anon$7: Ref
+    var anon$23: Ref
     var ret$17: Ref
-    var anon$17: Ref
+    var anon$8: Ref
+    var anon$24: Ref
     var ret$18: Ref
-    var anon$4: Ref
-    var anon$18: Ref
+    var anon$9: Ref
+    var anon$25: Ref
     var ret$19: Ref
-    anon$2 := df$rt$intToRef(1)
-    anon$3 := sp$plusInts(anon$2, df$rt$intToRef(1))
-    anon$4 := sp$plusInts(anon$3, df$rt$intToRef(1))
-    ret$19 := sp$plusInts(anon$4, df$rt$intToRef(1))
+    var anon$10: Ref
+    anon$4 := df$rt$intToRef(1)
+    inhale df$rt$isSubtype(df$rt$typeOf(anon$4), df$rt$nullable(df$rt$anyType()))
+    anon$5 := anon$4
+    inhale df$rt$isSubtype(df$rt$typeOf(anon$5), df$rt$intType())
+    anon$6 := anon$5
+    anon$7 := sp$plusInts(anon$6, df$rt$intToRef(1))
+    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$intType())
+    anon$8 := anon$7
+    anon$9 := sp$plusInts(anon$8, df$rt$intToRef(1))
+    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$intType())
+    anon$10 := anon$9
+    ret$19 := sp$plusInts(anon$10, df$rt$intToRef(1))
     goto lbl$ret$19
     label lbl$ret$19
-    anon$18 := ret$19
-    ret$18 := anon$18
+    anon$25 := ret$19
+    ret$18 := anon$25
+    inhale df$rt$isSubtype(df$rt$typeOf(ret$18), df$rt$nullable(df$rt$anyType()))
     goto lbl$ret$18
     label lbl$ret$18
-    anon$17 := ret$18
-    ret$17 := anon$17
+    anon$24 := ret$18
+    ret$17 := anon$24
+    inhale df$rt$isSubtype(df$rt$typeOf(ret$17), df$rt$intType())
     goto lbl$ret$17
     label lbl$ret$17
-    anon$16 := ret$17
-    ret$16 := anon$16
+    anon$23 := ret$17
+    ret$16 := anon$23
+    inhale df$rt$isSubtype(df$rt$typeOf(ret$16), df$rt$nullable(df$rt$anyType()))
     goto lbl$ret$16
     label lbl$ret$16
-    anon$15 := ret$16
-    ret$15 := anon$15
+    anon$22 := ret$16
+    ret$15 := anon$22
+    inhale df$rt$isSubtype(df$rt$typeOf(ret$15), df$rt$intType())
     goto lbl$ret$15
     label lbl$ret$15
-    anon$14 := ret$15
-    ret$14 := anon$14
+    anon$21 := ret$15
+    ret$14 := anon$21
+    inhale df$rt$isSubtype(df$rt$typeOf(ret$14), df$rt$nullable(df$rt$anyType()))
     goto lbl$ret$14
     label lbl$ret$14
-    anon$13 := ret$14
-    ret$13 := anon$13
+    anon$20 := ret$14
+    ret$13 := anon$20
+    inhale df$rt$isSubtype(df$rt$typeOf(ret$13), df$rt$intType())
     goto lbl$ret$13
     label lbl$ret$13
     l15$result := ret$13
@@ -432,12 +499,14 @@ method f$complexScenario$TF$T$Boolean(p$arg: Ref) returns (ret$0: Ref)
     ret$11 := ret$12
     goto lbl$ret$11
     label lbl$ret$11
-    anon$12 := ret$11
-    ret$10 := anon$12
+    anon$19 := ret$11
+    ret$10 := anon$19
+    inhale df$rt$isSubtype(df$rt$typeOf(ret$10), df$rt$nullable(df$rt$anyType()))
     goto lbl$ret$10
     label lbl$ret$10
-    anon$11 := ret$10
-    ret$0 := anon$11
+    anon$18 := ret$10
+    ret$0 := anon$18
+    inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$boolType())
   }
   goto lbl$ret$0
   label lbl$ret$0
@@ -458,33 +527,42 @@ method f$testCustomClass$TF$() returns (ret$0: Ref)
 {
   var l0$custom: Ref
   var anon$0: Ref
-  var ret$1: Ref
   var anon$1: Ref
-  var ret$2: Ref
+  var ret$1: Ref
   var anon$2: Ref
-  var ret$3: Ref
+  var ret$2: Ref
   var anon$3: Ref
+  var anon$4: Ref
+  var ret$3: Ref
+  var anon$5: Ref
   var ret$4: Ref
   l0$custom := con$c$CustomClass$()
   unfold acc(p$c$CustomClass$shared(l0$custom), wildcard)
   ret$2 := l0$custom.bf$member
   goto lbl$ret$2
   label lbl$ret$2
-  anon$1 := ret$2
-  ret$1 := anon$1
+  anon$2 := ret$2
+  ret$1 := anon$2
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$1), df$rt$nullable(df$rt$anyType()))
   goto lbl$ret$1
   label lbl$ret$1
-  anon$0 := ret$1
+  anon$1 := ret$1
+  anon$0 := anon$1
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$0), df$rt$intType())
   unfold acc(p$c$CustomClass$shared(l0$custom), wildcard)
   ret$4 := l0$custom.bf$member
   goto lbl$ret$4
   label lbl$ret$4
-  anon$3 := ret$4
-  ret$3 := anon$3
+  anon$5 := ret$4
+  ret$3 := anon$5
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$3), df$rt$nullable(df$rt$anyType()))
   goto lbl$ret$3
   label lbl$ret$3
-  anon$2 := ret$3
-  ret$0 := df$rt$boolToRef(anon$0 == anon$2)
+  anon$4 := ret$3
+  anon$3 := anon$4
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$3), df$rt$intType())
+  ret$0 := df$rt$boolToRef(df$rt$intFromRef(anon$0) ==
+    df$rt$intFromRef(anon$3))
   goto lbl$ret$0
   label lbl$ret$0
 }
diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/inline_correctness.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/good_contracts/inline_correctness.fir.diag.txt
index f57ee96b3e5f4..463e46631306e 100644
--- a/plugins/formal-verification/testData/diagnostics/good_contracts/inline_correctness.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/good_contracts/inline_correctness.fir.diag.txt
@@ -135,9 +135,11 @@ method f$named_double_nonlocal_return$TF$() returns (ret$0: Ref)
   ret$0 := df$rt$boolToRef(false)
   goto lbl$ret$0
   label lbl$ret$4
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$4), df$rt$unitType())
   ret$3 := ret$4
   goto lbl$ret$3
   label lbl$ret$3
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$3), df$rt$unitType())
   ret$0 := df$rt$boolToRef(false)
   goto lbl$ret$0
   ret$2 := df$rt$boolToRef(true)
diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/is_type_contract.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/good_contracts/is_type_contract.fir.diag.txt
index 1478c04d647ea..87a7ac8640f73 100644
--- a/plugins/formal-verification/testData/diagnostics/good_contracts/is_type_contract.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/good_contracts/is_type_contract.fir.diag.txt
@@ -39,8 +39,8 @@ method f$subtypeTransitive$TF$T$Unit(p$x: Ref) returns (ret$0: Ref)
     df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$nullable(df$rt$anyType()))
 {
   inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$unitType())
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /is_type_contract.kt:(870,891): info: Generated Viper text for constructorReturnType:
@@ -72,8 +72,8 @@ method f$subtypeSuperType$TF$T$c$Bar(p$bar: Ref) returns (ret$0: Ref)
 {
   inhale df$rt$isSubtype(df$rt$typeOf(p$bar), df$rt$T$c$Bar())
   inhale acc(p$c$Bar$shared(p$bar), wildcard)
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /is_type_contract.kt:(1149,1160): info: Generated Viper text for typeOfField:
diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/list.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/good_contracts/list.fir.diag.txt
index fe50a8e3ff0ea..e27308f84fcc8 100644
--- a/plugins/formal-verification/testData/diagnostics/good_contracts/list.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/good_contracts/list.fir.diag.txt
@@ -7,8 +7,8 @@ method f$declaration$TF$() returns (ret$0: Ref)
   var l0$l1: Ref
   var l0$l2: Ref
   var l0$l3: Ref
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /list.kt:(187,201): info: Generated Viper text for initialization:
@@ -26,10 +26,10 @@ method f$initialization$TF$T$c$pkg$kotlin_collections$List(p$l: Ref)
   var l0$myEmptyList: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$l), df$rt$T$c$pkg$kotlin_collections$List())
   inhale acc(p$pkg$kotlin_collections$c$List$shared(p$l), wildcard)
-  ret$0 := df$rt$unitValue()
   l0$myList := p$l
   l0$myEmptyList := f$pkg$kotlin_collections$emptyList$TF$()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method f$pkg$kotlin_collections$emptyList$TF$() returns (ret: Ref)
@@ -55,12 +55,12 @@ method f$add_get$TF$T$c$pkg$kotlin_collections$MutableList(p$l: Ref)
   var l0$n: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$l), df$rt$T$c$pkg$kotlin_collections$MutableList())
   inhale acc(p$pkg$kotlin_collections$c$MutableList$shared(p$l), wildcard)
-  ret$0 := df$rt$unitValue()
   anon$0 := f$pkg$kotlin_collections$c$MutableList$add$TF$T$c$pkg$kotlin_collections$MutableList$T$Int(p$l,
     df$rt$intToRef(1))
   l0$n := f$pkg$kotlin_collections$c$MutableList$get$TF$T$c$pkg$kotlin_collections$MutableList$T$Int(p$l,
     df$rt$intToRef(0))
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method f$pkg$kotlin_collections$c$MutableList$add$TF$T$c$pkg$kotlin_collections$MutableList$T$Int(this: Ref,
@@ -198,7 +198,6 @@ method f$nullable_list$TF$c$pkg$kotlin_collections$List(p$l: Ref)
   inhale df$rt$isSubtype(df$rt$typeOf(p$l), df$rt$nullable(df$rt$T$c$pkg$kotlin_collections$List()))
   inhale p$l != df$rt$nullValue() ==>
     acc(p$pkg$kotlin_collections$c$List$shared(p$l), wildcard)
-  ret$0 := df$rt$unitValue()
   if (!(p$l == df$rt$nullValue())) {
     var anon$1: Ref
     anon$1 := f$pkg$kotlin_collections$c$List$isEmpty$TF$T$c$pkg$kotlin_collections$List(p$l)
@@ -214,6 +213,7 @@ method f$nullable_list$TF$c$pkg$kotlin_collections$List(p$l: Ref)
       sp$minusInts(anon$2, df$rt$intToRef(1)))
   }
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method f$pkg$kotlin_collections$c$List$get$TF$T$c$pkg$kotlin_collections$List$T$Int(this: Ref,
diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/multiple_interfaces.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/good_contracts/multiple_interfaces.fir.diag.txt
index e0cdd2c2bf5ce..3035c6976c8ca 100644
--- a/plugins/formal-verification/testData/diagnostics/good_contracts/multiple_interfaces.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/good_contracts/multiple_interfaces.fir.diag.txt
@@ -7,11 +7,11 @@ method f$take1$TF$T$c$InterfaceWithImplementation1(p$obj: Ref)
   var anon$1: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$obj), df$rt$T$c$InterfaceWithImplementation1())
   inhale acc(p$c$InterfaceWithImplementation1$shared(p$obj), wildcard)
-  ret$0 := df$rt$unitValue()
   anon$1 := pg$public$field(p$obj)
   anon$0 := anon$1
   inhale df$rt$isSubtype(df$rt$typeOf(anon$0), df$rt$intType())
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method pg$public$field(this: Ref) returns (ret: Ref)
@@ -26,11 +26,11 @@ method f$take2$TF$T$c$InterfaceWithoutImplementation2(p$obj: Ref)
   var anon$1: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$obj), df$rt$T$c$InterfaceWithoutImplementation2())
   inhale acc(p$c$InterfaceWithoutImplementation2$shared(p$obj), wildcard)
-  ret$0 := df$rt$unitValue()
   anon$1 := pg$public$field(p$obj)
   anon$0 := anon$1
   inhale df$rt$isSubtype(df$rt$typeOf(anon$0), df$rt$intType())
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method pg$public$field(this: Ref) returns (ret: Ref)
@@ -45,8 +45,8 @@ method f$take3$TF$T$c$AbstractWithFinalImplementation3(p$obj: Ref)
 {
   inhale df$rt$isSubtype(df$rt$typeOf(p$obj), df$rt$T$c$AbstractWithFinalImplementation3())
   inhale acc(p$c$AbstractWithFinalImplementation3$shared(p$obj), wildcard)
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /multiple_interfaces.kt:(1025,1030): info: Generated Viper text for take4:
@@ -58,11 +58,11 @@ method f$take4$TF$T$c$AbstractWithOpenImplementation4(p$obj: Ref)
   var anon$1: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$obj), df$rt$T$c$AbstractWithOpenImplementation4())
   inhale acc(p$c$AbstractWithOpenImplementation4$shared(p$obj), wildcard)
-  ret$0 := df$rt$unitValue()
   anon$1 := pg$public$field(p$obj)
   anon$0 := anon$1
   inhale df$rt$isSubtype(df$rt$typeOf(anon$0), df$rt$intType())
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method pg$public$field(this: Ref) returns (ret: Ref)
diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/override_properties_types.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/good_contracts/override_properties_types.fir.diag.txt
index fa8c5a3429aea..54499b559f5f2 100644
--- a/plugins/formal-verification/testData/diagnostics/good_contracts/override_properties_types.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/good_contracts/override_properties_types.fir.diag.txt
@@ -49,4 +49,3 @@ method pg$public$field(this: Ref) returns (ret: Ref)
 
 
 method ps$public$field(this: Ref, anon$0: Ref) returns (ret: Ref)
-
diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/private_properties.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/good_contracts/private_properties.fir.diag.txt
index 5f6e8e3cb0b8b..e24258cb15b35 100644
--- a/plugins/formal-verification/testData/diagnostics/good_contracts/private_properties.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/good_contracts/private_properties.fir.diag.txt
@@ -94,4 +94,3 @@ method pg$public$length(this: Ref) returns (ret: Ref)
 
 
 method ps$c$A$private$field(this: Ref, anon$0: Ref) returns (ret: Ref)
-
diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/simple.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/good_contracts/simple.fir.diag.txt
index 66dc37f9edbff..64b21b9a9d46e 100644
--- a/plugins/formal-verification/testData/diagnostics/good_contracts/simple.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/good_contracts/simple.fir.diag.txt
@@ -2,8 +2,8 @@
 method f$without_contract$TF$() returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /simple.kt:(148,161): info: Generated Viper text for with_contract:
@@ -11,6 +11,6 @@ method f$with_contract$TF$() returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
   ensures true
 {
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/unit_return_type.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/good_contracts/unit_return_type.fir.diag.txt
new file mode 100644
index 0000000000000..e1621be0972b4
--- /dev/null
+++ b/plugins/formal-verification/testData/diagnostics/good_contracts/unit_return_type.fir.diag.txt
@@ -0,0 +1,73 @@
+/unit_return_type.kt:(171,176): info: Generated Viper text for idFun:
+method f$idFun$TF$Any(p$t: Ref) returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$nullable(df$rt$anyType()))
+{
+  inhale df$rt$isSubtype(df$rt$typeOf(p$t), df$rt$nullable(df$rt$anyType()))
+  ret$0 := p$t
+  goto lbl$ret$0
+  label lbl$ret$0
+}
+
+/unit_return_type.kt:(195,208): info: Generated Viper text for directReturns:
+method f$directReturns$TF$T$Boolean(p$b: Ref) returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
+{
+  inhale df$rt$isSubtype(df$rt$typeOf(p$b), df$rt$boolType())
+  if (df$rt$boolFromRef(p$b)) {
+    ret$0 := df$rt$unitValue()
+    goto lbl$ret$0
+  } else {
+    var anon$0: Ref
+    var anon$1: Ref
+    anon$1 := f$idFun$TF$Any(p$b)
+    anon$0 := anon$1
+    inhale df$rt$isSubtype(df$rt$typeOf(anon$0), df$rt$boolType())
+    if (df$rt$boolFromRef(anon$0)) {
+      ret$0 := df$rt$unitValue()
+      goto lbl$ret$0
+    }
+  }
+  label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
+}
+
+method f$idFun$TF$Any(p$t: Ref) returns (ret: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$nullable(df$rt$anyType()))
+
+
+/unit_return_type.kt:(374,387): info: Generated Viper text for useInlineUnit:
+method f$idFun$TF$Any(p$t: Ref) returns (ret: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$nullable(df$rt$anyType()))
+
+
+method f$useInlineUnit$TF$T$Boolean(p$b: Ref) returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
+{
+  var l0$unitRes: Ref
+  var ret$1: Ref
+  var anon$0: Ref
+  var ret$2: Ref
+  var anon$1: Ref
+  inhale df$rt$isSubtype(df$rt$typeOf(p$b), df$rt$boolType())
+  inhale df$rt$isSubtype(df$rt$typeOf(p$b), df$rt$nullable(df$rt$anyType()))
+  anon$0 := p$b
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$0), df$rt$boolType())
+  anon$1 := anon$0
+  if (df$rt$boolFromRef(anon$1)) {
+    var l4$tmp: Ref
+    var anon$2: Ref
+    var anon$3: Ref
+    l4$tmp := df$rt$intToRef(42)
+    anon$3 := f$idFun$TF$Any(l4$tmp)
+    anon$2 := anon$3
+    inhale df$rt$isSubtype(df$rt$typeOf(anon$2), df$rt$intType())
+  }
+  label lbl$ret$2
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$2), df$rt$unitType())
+  label lbl$ret$1
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$1), df$rt$unitType())
+  l0$unitRes := ret$1
+  assert l0$unitRes == df$rt$unitValue()
+  label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
+}
diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/unit_return_type.kt b/plugins/formal-verification/testData/diagnostics/good_contracts/unit_return_type.kt
new file mode 100644
index 0000000000000..6fb67b2427c19
--- /dev/null
+++ b/plugins/formal-verification/testData/diagnostics/good_contracts/unit_return_type.kt
@@ -0,0 +1,26 @@
+import org.jetbrains.kotlin.formver.plugin.NeverConvert
+import org.jetbrains.kotlin.formver.plugin.AlwaysVerify
+import org.jetbrains.kotlin.formver.plugin.verify
+
+fun <T> <!VIPER_TEXT!>idFun<!>(t: T): T = t
+
+fun <!VIPER_TEXT!>directReturns<!>(b: Boolean) {
+    if (b) return
+    else if (idFun(b)) return Unit
+}
+
+@NeverConvert
+inline fun <T> T.unitRun(block: T.() -> Unit) {
+    block()
+}
+
+@AlwaysVerify
+fun <!VIPER_TEXT!>useInlineUnit<!>(b: Boolean) {
+    val unitRes = b.unitRun {
+        if (this) {
+            val tmp = 42
+            idFun(tmp)
+        }
+    }
+    verify(unitRes == Unit)
+}
\ No newline at end of file
diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/viper_casts_while_inlining.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/good_contracts/viper_casts_while_inlining.fir.diag.txt
new file mode 100644
index 0000000000000..fd7022d309284
--- /dev/null
+++ b/plugins/formal-verification/testData/diagnostics/good_contracts/viper_casts_while_inlining.fir.diag.txt
@@ -0,0 +1,439 @@
+/viper_casts_while_inlining.kt:(250,255): info: Generated Viper text for idFun:
+method f$idFun$TF$Any(p$arg: Ref) returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$nullable(df$rt$anyType()))
+{
+  inhale df$rt$isSubtype(df$rt$typeOf(p$arg), df$rt$nullable(df$rt$anyType()))
+  ret$0 := p$arg
+  goto lbl$ret$0
+  label lbl$ret$0
+}
+
+/viper_casts_while_inlining.kt:(609,626): info: Generated Viper text for checkMemberAccess:
+field bf$member: Ref
+
+method con$c$ClassWithMember$T$Int(p$member: Ref) returns (ret: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$T$c$ClassWithMember())
+  ensures acc(p$c$ClassWithMember$shared(ret), wildcard)
+  ensures acc(p$c$ClassWithMember$unique(ret), write)
+  ensures (unfolding acc(p$c$ClassWithMember$shared(ret), wildcard) in
+      df$rt$intFromRef(ret.bf$member) == df$rt$intFromRef(p$member))
+
+
+method f$checkMemberAccess$TF$() returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$boolType())
+  ensures df$rt$boolFromRef(ret$0) == true
+{
+  var l0$obj: Ref
+  var anon$4: Ref
+  var anon$5: Ref
+  var ret$1: Ref
+  var anon$0: Ref
+  var anon$6: Ref
+  var ret$2: Ref
+  var anon$1: Ref
+  var anon$7: Ref
+  var anon$8: Ref
+  var anon$9: Ref
+  var ret$3: Ref
+  var anon$2: Ref
+  var anon$10: Ref
+  var ret$4: Ref
+  var anon$3: Ref
+  var anon$11: Ref
+  l0$obj := con$c$ClassWithMember$T$Int(df$rt$intToRef(42))
+  inhale df$rt$isSubtype(df$rt$typeOf(l0$obj), df$rt$nullable(df$rt$anyType()))
+  anon$0 := l0$obj
+  anon$7 := f$idFun$TF$Any(anon$0)
+  anon$1 := anon$7
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$1), df$rt$T$c$ClassWithMember())
+  inhale acc(p$c$ClassWithMember$shared(anon$1), wildcard)
+  unfold acc(p$c$ClassWithMember$shared(anon$1), wildcard)
+  ret$2 := anon$1.bf$member
+  goto lbl$ret$2
+  label lbl$ret$2
+  anon$6 := ret$2
+  ret$1 := anon$6
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$1), df$rt$nullable(df$rt$anyType()))
+  goto lbl$ret$1
+  label lbl$ret$1
+  anon$5 := ret$1
+  anon$4 := anon$5
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$4), df$rt$intType())
+  inhale df$rt$isSubtype(df$rt$typeOf(l0$obj), df$rt$nullable(df$rt$anyType()))
+  anon$2 := l0$obj
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$2), df$rt$T$c$ClassWithMember())
+  inhale acc(p$c$ClassWithMember$shared(anon$2), wildcard)
+  anon$3 := anon$2
+  unfold acc(p$c$ClassWithMember$shared(l0$obj), wildcard)
+  anon$11 := l0$obj.bf$member
+  ret$0 := df$rt$boolToRef(df$rt$intFromRef(anon$11) == 42)
+  goto lbl$ret$0
+  label lbl$ret$4
+  anon$10 := ret$4
+  ret$3 := anon$10
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$3), df$rt$nullable(df$rt$anyType()))
+  goto lbl$ret$3
+  label lbl$ret$3
+  anon$9 := ret$3
+  anon$8 := anon$9
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$8), df$rt$nothingType())
+  label lbl$ret$0
+}
+
+method f$idFun$TF$Any(p$arg: Ref) returns (ret: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$nullable(df$rt$anyType()))
+
+
+/viper_casts_while_inlining.kt:(895,919): info: Generated Viper text for checkGenericMemberAccess:
+field bf$wrapped: Ref
+
+method con$c$Box$Any(p$wrapped: Ref) returns (ret: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$T$c$Box())
+  ensures acc(p$c$Box$shared(ret), wildcard)
+  ensures acc(p$c$Box$unique(ret), write)
+  ensures (unfolding acc(p$c$Box$shared(ret), wildcard) in
+      ret.bf$wrapped == p$wrapped)
+
+
+method f$checkGenericMemberAccess$TF$T$c$Box(p$box: Ref)
+  returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$boolType())
+  ensures df$rt$boolFromRef(ret$0) == true
+{
+  var ret$1: Ref
+  var anon$0: Ref
+  var ret$2: Ref
+  var anon$1: Ref
+  var anon$4: Ref
+  var anon$5: Ref
+  var anon$6: Ref
+  var ret$3: Ref
+  var anon$2: Ref
+  var anon$7: Ref
+  var anon$8: Ref
+  var anon$9: Ref
+  var ret$4: Ref
+  var anon$3: Ref
+  var anon$10: Ref
+  var anon$11: Ref
+  inhale df$rt$isSubtype(df$rt$typeOf(p$box), df$rt$T$c$Box())
+  inhale acc(p$c$Box$shared(p$box), wildcard)
+  inhale df$rt$isSubtype(df$rt$typeOf(p$box), df$rt$nullable(df$rt$anyType()))
+  anon$0 := p$box
+  anon$4 := f$idFun$TF$Any(anon$0)
+  anon$1 := anon$4
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$1), df$rt$T$c$Box())
+  inhale acc(p$c$Box$shared(anon$1), wildcard)
+  unfold acc(p$c$Box$shared(anon$1), wildcard)
+  ret$2 := anon$1.bf$wrapped
+  goto lbl$ret$2
+  label lbl$ret$2
+  ret$1 := ret$2
+  goto lbl$ret$1
+  label lbl$ret$1
+  unfold acc(p$c$Box$shared(p$box), wildcard)
+  anon$8 := p$box.bf$wrapped
+  anon$7 := con$c$Box$Any(anon$8)
+  anon$2 := anon$7
+  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$T$c$Box())
+  inhale acc(p$c$Box$shared(anon$2), wildcard)
+  anon$3 := anon$2
+  unfold acc(p$c$Box$shared(anon$3), wildcard)
+  anon$10 := anon$3.bf$wrapped
+  unfold acc(p$c$Box$shared(p$box), wildcard)
+  anon$11 := p$box.bf$wrapped
+  ret$0 := df$rt$boolToRef(anon$10 == anon$11)
+  goto lbl$ret$0
+  label lbl$ret$4
+  anon$9 := ret$4
+  ret$3 := anon$9
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$3), df$rt$nullable(df$rt$anyType()))
+  goto lbl$ret$3
+  label lbl$ret$3
+  anon$6 := ret$3
+  anon$5 := anon$6
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$5), df$rt$nothingType())
+  label lbl$ret$0
+}
+
+method f$idFun$TF$Any(p$arg: Ref) returns (ret: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$nullable(df$rt$anyType()))
+
+
+/viper_casts_while_inlining.kt:(1161,1182): info: Generated Viper text for checkArgumentIsCopied:
+field bf$a: Ref
+
+method f$checkArgumentIsCopied$TF$T$c$ClassWithVar(p$x: Ref)
+  returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
+{
+  var anon$2: Ref
+  var anon$3: Ref
+  var ret$1: Ref
+  var anon$0: Ref
+  var anon$4: Ref
+  var anon$5: Ref
+  var ret$2: Ref
+  var anon$1: Ref
+  inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$T$c$ClassWithVar())
+  inhale acc(p$c$ClassWithVar$shared(p$x), wildcard)
+  inhale acc(p$x.bf$a, write)
+  anon$4 := p$x.bf$a
+  exhale acc(p$x.bf$a, write)
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$4), df$rt$intType())
+  anon$0 := anon$4
+  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$intType())
+  anon$1 := anon$0
+  inhale acc(p$x.bf$a, write)
+  p$x.bf$a := df$rt$intToRef(42)
+  exhale acc(p$x.bf$a, write)
+  ret$2 := anon$1
+  goto lbl$ret$2
+  label lbl$ret$2
+  anon$5 := ret$2
+  ret$1 := anon$5
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$1), df$rt$nullable(df$rt$anyType()))
+  goto lbl$ret$1
+  label lbl$ret$1
+  anon$3 := ret$1
+  anon$2 := anon$3
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$2), df$rt$intType())
+  label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
+}
+
+/viper_casts_while_inlining.kt:(1347,1364): info: Generated Viper text for accessManyMembers:
+field bf$a: Ref
+
+field bf$b: Ref
+
+field bf$c: Ref
+
+field bf$i: Ref
+
+method f$accessManyMembers$TF$T$c$ManyMembers(p$m: Ref)
+  returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
+{
+  var anon$4: Ref
+  var anon$5: Ref
+  var ret$1: Ref
+  var anon$0: Ref
+  var anon$6: Ref
+  var ret$2: Ref
+  var anon$1: Ref
+  var anon$7: Ref
+  var anon$8: Ref
+  var anon$9: Ref
+  var anon$10: Ref
+  var anon$11: Ref
+  var anon$12: Ref
+  var anon$13: Ref
+  var anon$14: Ref
+  var ret$3: Ref
+  var anon$2: Ref
+  var anon$15: Ref
+  var ret$4: Ref
+  var anon$3: Ref
+  var anon$16: Ref
+  var anon$17: Ref
+  var anon$18: Ref
+  var anon$19: Ref
+  var anon$20: Ref
+  var anon$21: Ref
+  var anon$22: Ref
+  inhale df$rt$isSubtype(df$rt$typeOf(p$m), df$rt$T$c$ManyMembers())
+  inhale acc(p$c$ManyMembers$shared(p$m), wildcard)
+  inhale df$rt$isSubtype(df$rt$typeOf(p$m), df$rt$nullable(df$rt$anyType()))
+  anon$0 := p$m
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$0), df$rt$T$c$ManyMembers())
+  inhale acc(p$c$ManyMembers$shared(anon$0), wildcard)
+  anon$1 := anon$0
+  unfold acc(p$c$ManyMembers$shared(anon$1), wildcard)
+  anon$9 := anon$1.bf$i
+  anon$8 := f$idFun$TF$Any(anon$9)
+  anon$7 := anon$8
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$7), df$rt$intType())
+  inhale acc(anon$1.bf$b, write)
+  anon$12 := anon$1.bf$b
+  exhale acc(anon$1.bf$b, write)
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$12), df$rt$boolType())
+  anon$11 := f$idFun$TF$Any(anon$12)
+  anon$10 := anon$11
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$10), df$rt$boolType())
+  unfold acc(p$c$ManyMembers$shared(anon$1), wildcard)
+  ret$2 := anon$1.bf$c
+  goto lbl$ret$2
+  label lbl$ret$2
+  anon$6 := ret$2
+  ret$1 := anon$6
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$1), df$rt$nullable(df$rt$anyType()))
+  goto lbl$ret$1
+  label lbl$ret$1
+  anon$5 := ret$1
+  anon$4 := anon$5
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$4), df$rt$T$c$ClassWithVar())
+  inhale acc(p$c$ClassWithVar$shared(anon$4), wildcard)
+  inhale df$rt$isSubtype(df$rt$typeOf(p$m), df$rt$nullable(df$rt$anyType()))
+  anon$2 := p$m
+  anon$16 := f$idFun$TF$Any(anon$2)
+  anon$3 := anon$16
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$3), df$rt$T$c$ManyMembers())
+  inhale acc(p$c$ManyMembers$shared(anon$3), wildcard)
+  unfold acc(p$c$ManyMembers$shared(anon$3), wildcard)
+  anon$19 := anon$3.bf$i
+  anon$18 := f$idFun$TF$Any(anon$19)
+  anon$17 := anon$18
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$17), df$rt$intType())
+  inhale acc(anon$3.bf$b, write)
+  anon$22 := anon$3.bf$b
+  exhale acc(anon$3.bf$b, write)
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$22), df$rt$boolType())
+  anon$21 := f$idFun$TF$Any(anon$22)
+  anon$20 := anon$21
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$20), df$rt$boolType())
+  unfold acc(p$c$ManyMembers$shared(anon$3), wildcard)
+  ret$4 := anon$3.bf$c
+  goto lbl$ret$4
+  label lbl$ret$4
+  anon$15 := ret$4
+  ret$3 := anon$15
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$3), df$rt$nullable(df$rt$anyType()))
+  goto lbl$ret$3
+  label lbl$ret$3
+  anon$14 := ret$3
+  anon$13 := anon$14
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$13), df$rt$T$c$ClassWithVar())
+  inhale acc(p$c$ClassWithVar$shared(anon$13), wildcard)
+  label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
+}
+
+method f$idFun$TF$Any(p$arg: Ref) returns (ret: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$nullable(df$rt$anyType()))
+
+
+/viper_casts_while_inlining.kt:(1540,1558): info: Generated Viper text for checkEvaluatedOnce:
+field bf$a: Ref
+
+field bf$b: Ref
+
+field bf$c: Ref
+
+field bf$i: Ref
+
+method f$checkEvaluatedOnce$TF$T$Int$T$c$ManyMembers(p$i: Ref, p$mm: Ref)
+  returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
+{
+  var anon$2: Ref
+  var anon$3: Ref
+  var ret$1: Ref
+  var anon$0: Ref
+  var anon$4: Ref
+  var anon$5: Ref
+  var anon$6: Ref
+  var ret$2: Ref
+  var anon$1: Ref
+  inhale df$rt$isSubtype(df$rt$typeOf(p$i), df$rt$intType())
+  inhale df$rt$isSubtype(df$rt$typeOf(p$mm), df$rt$T$c$ManyMembers())
+  inhale acc(p$c$ManyMembers$shared(p$mm), wildcard)
+  inhale acc(p$mm.bf$b, write)
+  anon$5 := p$mm.bf$b
+  exhale acc(p$mm.bf$b, write)
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$5), df$rt$boolType())
+  if (df$rt$boolFromRef(anon$5)) {
+    anon$4 := df$rt$intToRef(1)
+  } else {
+    anon$4 := df$rt$intToRef(-1)}
+  anon$0 := sp$plusInts(p$i, anon$4)
+  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$intType())
+  anon$1 := anon$0
+  assert df$rt$intFromRef(anon$1) == df$rt$intFromRef(anon$1)
+  label lbl$ret$2
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$2), df$rt$unitType())
+  anon$6 := ret$2
+  ret$1 := anon$6
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$1), df$rt$nullable(df$rt$anyType()))
+  goto lbl$ret$1
+  label lbl$ret$1
+  anon$3 := ret$1
+  anon$2 := anon$3
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$2), df$rt$unitType())
+  label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
+}
+
+/viper_casts_while_inlining.kt:(1686,1693): info: Generated Viper text for useRuns:
+method f$useRuns$TF$T$Int(p$x: Ref) returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
+{
+  var anon$4: Ref
+  var anon$5: Ref
+  var ret$1: Ref
+  var anon$6: Ref
+  var ret$2: Ref
+  var anon$7: Ref
+  var anon$8: Ref
+  var ret$3: Ref
+  var anon$0: Ref
+  var anon$9: Ref
+  var ret$4: Ref
+  var anon$1: Ref
+  var anon$10: Ref
+  var anon$11: Ref
+  var ret$5: Ref
+  var anon$2: Ref
+  var anon$12: Ref
+  var ret$6: Ref
+  var anon$3: Ref
+  inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$intType())
+  ret$2 := sp$plusInts(p$x, df$rt$intToRef(1))
+  goto lbl$ret$2
+  label lbl$ret$2
+  anon$6 := ret$2
+  ret$1 := anon$6
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$1), df$rt$nullable(df$rt$anyType()))
+  goto lbl$ret$1
+  label lbl$ret$1
+  anon$5 := ret$1
+  anon$4 := anon$5
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$4), df$rt$intType())
+  assert df$rt$intFromRef(anon$4) == 1 + df$rt$intFromRef(p$x)
+  inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$nullable(df$rt$anyType()))
+  anon$0 := p$x
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$0), df$rt$intType())
+  anon$1 := anon$0
+  ret$4 := sp$plusInts(anon$1, df$rt$intToRef(1))
+  goto lbl$ret$4
+  label lbl$ret$4
+  anon$9 := ret$4
+  ret$3 := anon$9
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$3), df$rt$nullable(df$rt$anyType()))
+  goto lbl$ret$3
+  label lbl$ret$3
+  anon$8 := ret$3
+  anon$7 := anon$8
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$7), df$rt$intType())
+  assert df$rt$intFromRef(anon$7) == 1 + df$rt$intFromRef(p$x)
+  anon$2 := sp$plusInts(p$x, df$rt$intToRef(1))
+  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$intType())
+  anon$3 := anon$2
+  assert df$rt$intFromRef(anon$3) == 1 + df$rt$intFromRef(p$x)
+  label lbl$ret$6
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$6), df$rt$unitType())
+  anon$12 := ret$6
+  ret$5 := anon$12
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$5), df$rt$nullable(df$rt$anyType()))
+  goto lbl$ret$5
+  label lbl$ret$5
+  anon$11 := ret$5
+  anon$10 := anon$11
+  inhale df$rt$isSubtype(df$rt$typeOf(anon$10), 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/good_contracts/viper_casts_while_inlining.kt b/plugins/formal-verification/testData/diagnostics/good_contracts/viper_casts_while_inlining.kt
new file mode 100644
index 0000000000000..b12dd40437e79
--- /dev/null
+++ b/plugins/formal-verification/testData/diagnostics/good_contracts/viper_casts_while_inlining.kt
@@ -0,0 +1,91 @@
+import kotlin.contracts.ExperimentalContracts
+import kotlin.contracts.contract
+import org.jetbrains.kotlin.formver.plugin.NeverConvert
+import org.jetbrains.kotlin.formver.plugin.AlwaysVerify
+import org.jetbrains.kotlin.formver.plugin.verify
+
+fun <T> <!VIPER_TEXT!>idFun<!>(arg: T): T = arg
+
+@NeverConvert
+public inline fun <T, R> T.runWithId(block: T.() -> R): R = idFun(this).block()
+
+@NeverConvert
+public inline fun <T, R> T.copiedRun(block: T.() -> R): R = block()
+
+@NeverConvert
+public inline fun <T> copiedRun(block: () -> T): T = block()
+
+class ClassWithMember(val member: Int)
+
+@OptIn(ExperimentalContracts::class)
+fun <!VIPER_TEXT!>checkMemberAccess<!>(): Boolean {
+    contract {
+        returns(true)
+    }
+
+    val obj = ClassWithMember(42)
+    obj.runWithId {
+        member
+    }
+    obj.copiedRun {
+        return obj.member == 42
+    }
+}
+
+class Box<T>(val wrapped: T)
+
+@OptIn(ExperimentalContracts::class)
+fun <T> <!VIPER_TEXT!>checkGenericMemberAccess<!>(box: Box<T>): Boolean {
+    contract {
+        returns(true)
+    }
+
+    box.runWithId {
+        wrapped
+    }
+
+    Box(box.wrapped).copiedRun {
+        return wrapped == box.wrapped
+    }
+}
+
+class ClassWithVar(var a: Int)
+
+@AlwaysVerify
+fun <!VIPER_TEXT!>checkArgumentIsCopied<!>(x: ClassWithVar) {
+    x.a.copiedRun {
+        x.a = 42
+        this
+    }
+}
+
+class ManyMembers(val i: Int, var b: Boolean, val c: ClassWithVar)
+
+@AlwaysVerify
+fun <!VIPER_TEXT!>accessManyMembers<!>(m: ManyMembers) {
+    m.copiedRun {
+        idFun(i)
+        idFun(b)
+        c
+    }
+    m.runWithId {
+        idFun(i)
+        idFun(b)
+        c
+    }
+}
+
+@AlwaysVerify
+fun <!VIPER_TEXT!>checkEvaluatedOnce<!>(i: Int, mm: ManyMembers) {
+    (i + (if (mm.b) 1 else -1)).copiedRun {
+        verify(this == this)
+    }
+}
+
+@AlwaysVerify
+fun <!VIPER_TEXT!>useRuns<!>(x: Int): Unit {
+    verify(copiedRun { x + 1 } == 1 + x)
+    verify(x.copiedRun { plus(1) } == 1 + x)
+    (x + 1).copiedRun { verify(this == 1 + x) }
+}
+
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/basic.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/basic.fir.diag.txt
index 7549364e50cbb..ec6a6eb301de4 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/basic.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/basic.fir.diag.txt
@@ -2,8 +2,8 @@
 method f$returnUnit$TF$() returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /basic.kt:(43,52): info: Generated Viper text for returnInt:
@@ -20,8 +20,8 @@ method f$takeIntReturnUnit$TF$T$Int(p$x: Ref) returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$intType())
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /basic.kt:(140,156): info: Generated Viper text for takeIntReturnInt:
@@ -60,8 +60,8 @@ method f$intAssignment$TF$() returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   var l0$x: Ref
-  ret$0 := df$rt$unitValue()
   l0$x := df$rt$intToRef(0)
   l0$x := df$rt$intToRef(1)
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/field_getters.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/field_getters.fir.diag.txt
index d1c970db5ad84..f54b0da0f688b 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/field_getters.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/field_getters.fir.diag.txt
@@ -11,7 +11,6 @@ method f$testPrimitiveFieldGetter$TF$T$c$PrimitiveFields(p$pf: Ref)
   var l0$b: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$pf), df$rt$T$c$PrimitiveFields())
   inhale acc(p$c$PrimitiveFields$shared(p$pf), wildcard)
-  ret$0 := df$rt$unitValue()
   unfold acc(p$c$PrimitiveFields$shared(p$pf), wildcard)
   l0$a := p$pf.bf$a
   inhale acc(p$pf.bf$b, write)
@@ -19,6 +18,7 @@ method f$testPrimitiveFieldGetter$TF$T$c$PrimitiveFields(p$pf: Ref)
   exhale acc(p$pf.bf$b, write)
   inhale df$rt$isSubtype(df$rt$typeOf(l0$b), df$rt$intType())
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /field_getters.kt:(230,254): info: Generated Viper text for testReferenceFieldGetter:
@@ -42,7 +42,6 @@ method f$testReferenceFieldGetter$TF$T$c$ReferenceFields(p$rf: Ref)
   var l0$gb: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$rf), df$rt$T$c$ReferenceFields())
   inhale acc(p$c$ReferenceFields$shared(p$rf), wildcard)
-  ret$0 := df$rt$unitValue()
   unfold acc(p$c$ReferenceFields$shared(p$rf), wildcard)
   l0$f := p$rf.bf$f
   inhale acc(p$rf.bf$g, write)
@@ -63,6 +62,7 @@ method f$testReferenceFieldGetter$TF$T$c$ReferenceFields(p$rf: Ref)
   exhale acc(l0$g.bf$b, write)
   inhale df$rt$isSubtype(df$rt$typeOf(l0$gb), df$rt$intType())
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /field_getters.kt:(387,411): info: Generated Viper text for testCascadingFieldGetter:
@@ -88,7 +88,6 @@ method f$testCascadingFieldGetter$TF$T$c$ReferenceFields(p$rf: Ref)
   var anon$3: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$rf), df$rt$T$c$ReferenceFields())
   inhale acc(p$c$ReferenceFields$shared(p$rf), wildcard)
-  ret$0 := df$rt$unitValue()
   unfold acc(p$c$ReferenceFields$shared(p$rf), wildcard)
   anon$0 := p$rf.bf$f
   unfold acc(p$c$PrimitiveFields$shared(anon$0), wildcard)
@@ -116,4 +115,5 @@ method f$testCascadingFieldGetter$TF$T$c$ReferenceFields(p$rf: Ref)
   exhale acc(anon$3.bf$b, write)
   inhale df$rt$isSubtype(df$rt$typeOf(l0$gb), df$rt$intType())
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/inheritance.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/inheritance.fir.diag.txt
index 30b5423853de4..f189c47ba897b 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/inheritance.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/inheritance.fir.diag.txt
@@ -144,11 +144,11 @@ method f$setSuperField$TF$T$c$Bar(p$bar: Ref) returns (ret$0: Ref)
 {
   inhale df$rt$isSubtype(df$rt$typeOf(p$bar), df$rt$T$c$Bar())
   inhale acc(p$c$Bar$shared(p$bar), wildcard)
-  ret$0 := df$rt$unitValue()
   inhale acc(p$bar.bf$b, write)
   p$bar.bf$b := df$rt$boolToRef(true)
   exhale acc(p$bar.bf$b, write)
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /inheritance.kt:(525,546): info: Generated Viper text for accessSuperSuperField:
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/inheritance_fields.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/inheritance_fields.fir.diag.txt
index de71741395aa5..60e176240f57b 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/inheritance_fields.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/inheritance_fields.fir.diag.txt
@@ -21,7 +21,6 @@ method f$createB$TF$() returns (ret$0: Ref)
   var l0$fieldOverride: Ref
   var anon$0: Ref
   var l0$fieldNotOverride: Ref
-  ret$0 := df$rt$unitValue()
   l0$fieldB := con$c$FieldB$()
   l0$b := con$c$B$T$c$FieldB(l0$fieldB)
   anon$0 := pg$public$fieldOverride(l0$b)
@@ -32,6 +31,7 @@ method f$createB$TF$() returns (ret$0: Ref)
   unfold acc(p$c$A$shared(l0$b), wildcard)
   l0$fieldNotOverride := l0$b.bf$fieldNotOverride
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method pg$public$fieldOverride(this: Ref) returns (ret: Ref)
@@ -71,7 +71,6 @@ method f$createBFsAndNoBF$TF$() returns (ret$0: Ref)
   var anon$1: Ref
   var l0$sbf: Ref
   var l0$sbfx: Ref
-  ret$0 := df$rt$unitValue()
   l0$fbf := con$c$FirstBackingFieldClass$()
   anon$0 := pg$public$x(l0$fbf)
   l0$fbfx := anon$0
@@ -84,6 +83,7 @@ method f$createBFsAndNoBF$TF$() returns (ret$0: Ref)
   unfold acc(p$c$SecondBackingFieldClass$shared(l0$sbf), wildcard)
   l0$sbfx := l0$sbf.bf$x
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method pg$public$x(this: Ref) returns (ret: Ref)
@@ -103,10 +103,10 @@ method f$createY$TF$() returns (ret$0: Ref)
 {
   var l0$y: Ref
   var l0$ya: Ref
-  ret$0 := df$rt$unitValue()
   l0$y := con$c$Y$T$Int(df$rt$intToRef(10))
   unfold acc(p$c$Y$shared(l0$y), wildcard)
   unfold acc(p$c$X$shared(l0$y), wildcard)
   l0$ya := l0$y.bf$a
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/interface.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/interface.fir.diag.txt
index 1879552c11ed4..5b851548bd8a0 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/interface.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/interface.fir.diag.txt
@@ -10,7 +10,6 @@ method f$testProperties$TF$T$c$Foo(p$foo: Ref) returns (ret$0: Ref)
   var anon$4: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$foo), df$rt$T$c$Foo())
   inhale acc(p$c$Foo$shared(p$foo), wildcard)
-  ret$0 := df$rt$unitValue()
   anon$0 := ps$public$varProp(p$foo, df$rt$intToRef(0))
   anon$2 := pg$public$varProp(p$foo)
   anon$1 := anon$2
@@ -20,6 +19,7 @@ method f$testProperties$TF$T$c$Foo(p$foo: Ref) returns (ret$0: Ref)
   inhale df$rt$isSubtype(df$rt$typeOf(anon$3), df$rt$intType())
   l0$x := sp$plusInts(anon$1, anon$3)
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method pg$public$valProp(this: Ref) returns (ret: Ref)
@@ -47,11 +47,11 @@ method f$createImpl$TF$() returns (ret$0: Ref)
 {
   var l0$impl: Ref
   var l0$implField: Ref
-  ret$0 := df$rt$unitValue()
   l0$impl := con$c$Impl$T$Int(df$rt$intToRef(-1))
   unfold acc(p$c$Impl$shared(l0$impl), wildcard)
   l0$implField := l0$impl.bf$number
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method pg$public$number(this: Ref) returns (ret: Ref)
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/member_functions.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/member_functions.fir.diag.txt
index 5ad947d328ba1..d86832c180f7d 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/member_functions.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/member_functions.fir.diag.txt
@@ -21,9 +21,9 @@ method f$c$Foo$callMemberFun$TF$T$c$Foo(this: Ref) returns (ret$0: Ref)
   var anon$0: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(this), df$rt$T$c$Foo())
   inhale acc(p$c$Foo$shared(this), wildcard)
-  ret$0 := df$rt$unitValue()
   anon$0 := f$c$Foo$memberFun$TF$T$c$Foo(this)
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method f$c$Foo$memberFun$TF$T$c$Foo(this: Ref) returns (ret: Ref)
@@ -46,9 +46,9 @@ method f$c$Foo$siblingCall$TF$T$c$Foo$T$c$Foo(this: Ref, p$other: Ref)
   inhale acc(p$c$Foo$shared(this), wildcard)
   inhale df$rt$isSubtype(df$rt$typeOf(p$other), df$rt$T$c$Foo())
   inhale acc(p$c$Foo$shared(p$other), wildcard)
-  ret$0 := df$rt$unitValue()
   anon$0 := f$c$Foo$memberFun$TF$T$c$Foo(p$other)
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /member_functions.kt:(220,238): info: Generated Viper text for outerMemberFunCall:
@@ -64,7 +64,7 @@ method f$outerMemberFunCall$TF$T$c$Foo(p$f: Ref) returns (ret$0: Ref)
   var anon$0: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$f), df$rt$T$c$Foo())
   inhale acc(p$c$Foo$shared(p$f), wildcard)
-  ret$0 := df$rt$unitValue()
   anon$0 := f$c$Foo$memberFun$TF$T$c$Foo(p$f)
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/multiple_interfaces.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/multiple_interfaces.fir.diag.txt
index fb29ed047720a..effd2da586ba4 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/multiple_interfaces.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/multiple_interfaces.fir.diag.txt
@@ -45,7 +45,6 @@ method f$testVarVal$TF$() returns (ret$0: Ref)
   var anon$3: Ref
   var anon$4: Ref
   var anon$5: Ref
-  ret$0 := df$rt$unitValue()
   l0$g := con$c$G$()
   anon$1 := pg$public$field(l0$g)
   anon$0 := anon$1
@@ -57,10 +56,10 @@ method f$testVarVal$TF$() returns (ret$0: Ref)
   inhale df$rt$isSubtype(df$rt$typeOf(anon$3), df$rt$intType())
   anon$5 := ps$public$field(l0$i, df$rt$intToRef(1))
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method pg$public$field(this: Ref) returns (ret: Ref)
 
 
 method ps$public$field(this: Ref, anon$0: Ref) returns (ret: Ref)
-
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/predicates.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/predicates.fir.diag.txt
index edfc9527ed316..1a499b9b76ba7 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/predicates.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/predicates.fir.diag.txt
@@ -63,8 +63,8 @@ method f$useClasses$TF$T$c$ReferenceField$T$c$Recursive(p$rf: Ref, p$rec: Ref)
   inhale acc(p$c$ReferenceField$shared(p$rf), wildcard)
   inhale df$rt$isSubtype(df$rt$typeOf(p$rec), df$rt$T$c$Recursive())
   inhale acc(p$c$Recursive$shared(p$rec), wildcard)
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /predicates.kt:(354,374): info: Generated Viper text for threeLayersHierarchy:
@@ -105,8 +105,8 @@ method f$threeLayersHierarchy$TF$T$c$C(p$c: Ref) returns (ret$0: Ref)
 {
   inhale df$rt$isSubtype(df$rt$typeOf(p$c), df$rt$T$c$C())
   inhale acc(p$c$C$shared(p$c), wildcard)
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /predicates.kt:(390,403): info: Generated Viper text for listHierarchy:
@@ -174,6 +174,6 @@ method f$listHierarchy$TF$T$c$pkg$kotlin_collections$MutableList(p$xs: Ref)
 {
   inhale df$rt$isSubtype(df$rt$typeOf(p$xs), df$rt$T$c$pkg$kotlin_collections$MutableList())
   inhale acc(p$pkg$kotlin_collections$c$MutableList$shared(p$xs), wildcard)
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/predicates_access.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/predicates_access.fir.diag.txt
index 251ad7fcc3021..d2655a51740d5 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/predicates_access.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/predicates_access.fir.diag.txt
@@ -60,12 +60,12 @@ method f$accessSuperTypeProperty$TF$T$c$C(p$c: Ref) returns (ret$0: Ref)
   var l0$temp: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$c), df$rt$T$c$C())
   inhale acc(p$c$C$shared(p$c), wildcard)
-  ret$0 := df$rt$unitValue()
   unfold acc(p$c$C$shared(p$c), wildcard)
   unfold acc(p$c$B$shared(p$c), wildcard)
   unfold acc(p$c$A$shared(p$c), wildcard)
   l0$temp := p$c.bf$a
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method pg$public$d(this: Ref) returns (ret: Ref)
@@ -134,12 +134,12 @@ method f$accessNested$TF$T$c$C(p$c: Ref) returns (ret$0: Ref)
   var anon$0: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$c), df$rt$T$c$C())
   inhale acc(p$c$C$shared(p$c), wildcard)
-  ret$0 := df$rt$unitValue()
   unfold acc(p$c$C$shared(p$c), wildcard)
   anon$0 := p$c.bf$x
   unfold acc(p$c$A$shared(anon$0), wildcard)
   l0$temp := anon$0.bf$a
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method pg$public$d(this: Ref) returns (ret: Ref)
@@ -164,12 +164,12 @@ method f$accessNullable$TF$c$A(p$x: Ref) returns (ret$0: Ref)
   var l0$n: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$nullable(df$rt$T$c$A()))
   inhale p$x != df$rt$nullValue() ==> acc(p$c$A$shared(p$x), wildcard)
-  ret$0 := df$rt$unitValue()
   if (!(p$x == df$rt$nullValue())) {
     unfold acc(p$c$A$shared(p$x), wildcard)
     l0$n := p$x.bf$a
   }
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /predicates_access.kt:(442,452): info: Generated Viper text for accessCast:
@@ -205,12 +205,12 @@ method f$accessCast$TF$T$c$A(p$x: Ref) returns (ret$0: Ref)
   var l0$n: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$T$c$A())
   inhale acc(p$c$A$shared(p$x), wildcard)
-  ret$0 := df$rt$unitValue()
   inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$T$c$B())
   inhale acc(p$c$B$shared(p$x), wildcard)
   unfold acc(p$c$B$shared(p$x), wildcard)
   l0$n := p$x.bf$b
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /predicates_access.kt:(501,515): info: Generated Viper text for accessSafeCast:
@@ -247,7 +247,6 @@ method f$accessSafeCast$TF$T$c$A(p$x: Ref) returns (ret$0: Ref)
   var l0$y: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$T$c$A())
   inhale acc(p$c$A$shared(p$x), wildcard)
-  ret$0 := df$rt$unitValue()
   l0$n := df$rt$intToRef(0)
   if (df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$T$c$B())) {
     l0$y := p$x
@@ -260,6 +259,7 @@ method f$accessSafeCast$TF$T$c$A(p$x: Ref) returns (ret$0: Ref)
     l0$n := l0$y.bf$b
   }
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /predicates_access.kt:(612,627): info: Generated Viper text for accessSmartCast:
@@ -295,7 +295,6 @@ method f$accessSmartCast$TF$T$c$A(p$x: Ref) returns (ret$0: Ref)
   var l0$n: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$T$c$A())
   inhale acc(p$c$A$shared(p$x), wildcard)
-  ret$0 := df$rt$unitValue()
   l0$n := df$rt$intToRef(0)
   if (df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$T$c$B())) {
     inhale acc(p$c$B$shared(p$x), wildcard)
@@ -303,4 +302,5 @@ method f$accessSmartCast$TF$T$c$A(p$x: Ref) returns (ret$0: Ref)
     l0$n := p$x.bf$b
   }
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/property_getters.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/property_getters.fir.diag.txt
index e25d105355c12..616e7b9e4e6b4 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/property_getters.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/property_getters.fir.diag.txt
@@ -27,7 +27,6 @@ method f$testReferencePropertyGetter$TF$T$c$ReferenceProperty(p$rp: Ref)
   var anon$1: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$rp), df$rt$T$c$ReferenceProperty())
   inhale acc(p$c$ReferenceProperty$shared(p$rp), wildcard)
-  ret$0 := df$rt$unitValue()
   anon$0 := pg$public$rProp(p$rp)
   l0$pp := anon$0
   inhale df$rt$isSubtype(df$rt$typeOf(l0$pp), df$rt$T$c$PrimitiveProperty())
@@ -36,6 +35,7 @@ method f$testReferencePropertyGetter$TF$T$c$ReferenceProperty(p$rp: Ref)
   l0$ppn := anon$1
   inhale df$rt$isSubtype(df$rt$typeOf(l0$ppn), df$rt$intType())
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method pg$public$nProp(this: Ref) returns (ret: Ref)
@@ -55,7 +55,6 @@ method f$testCascadingPropertyGetter$TF$T$c$ReferenceProperty(p$rp: Ref)
   var anon$2: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$rp), df$rt$T$c$ReferenceProperty())
   inhale acc(p$c$ReferenceProperty$shared(p$rp), wildcard)
-  ret$0 := df$rt$unitValue()
   anon$2 := pg$public$rProp(p$rp)
   anon$1 := anon$2
   inhale df$rt$isSubtype(df$rt$typeOf(anon$1), df$rt$T$c$PrimitiveProperty())
@@ -64,6 +63,7 @@ method f$testCascadingPropertyGetter$TF$T$c$ReferenceProperty(p$rp: Ref)
   l0$ppn := anon$0
   inhale df$rt$isSubtype(df$rt$typeOf(l0$ppn), df$rt$intType())
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method pg$public$nProp(this: Ref) returns (ret: Ref)
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/secondary_constructors.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/secondary_constructors.fir.diag.txt
index b81b2689859bd..b83321107e88a 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/secondary_constructors.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/secondary_constructors.fir.diag.txt
@@ -18,10 +18,10 @@ method f$onlySecondConstructors$TF$() returns (ret$0: Ref)
 {
   var l0$npc1: Ref
   var l0$npc2: Ref
-  ret$0 := df$rt$unitValue()
   l0$npc1 := con$c$NoPrimaryConstructor$T$Boolean(df$rt$boolToRef(true))
   l0$npc2 := con$c$NoPrimaryConstructor$T$Int(df$rt$intToRef(42))
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /secondary_constructors.kt:(365,392): info: Generated Viper text for primaryAndSecondConstructor:
@@ -46,8 +46,8 @@ method f$primaryAndSecondConstructor$TF$() returns (ret$0: Ref)
 {
   var l0$bc1: Ref
   var l0$bc2: Ref
-  ret$0 := df$rt$unitValue()
   l0$bc1 := con$c$BothConstructors$T$Boolean(df$rt$boolToRef(false))
   l0$bc2 := con$c$BothConstructors$T$Int(df$rt$intToRef(42))
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/setters.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/setters.fir.diag.txt
index 47004d475e9d7..d6bc7687c7c35 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/setters.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/setters.fir.diag.txt
@@ -7,11 +7,11 @@ method f$testPrimitiveFieldSetter$TF$T$c$PrimitiveField(p$pf: Ref)
 {
   inhale df$rt$isSubtype(df$rt$typeOf(p$pf), df$rt$T$c$PrimitiveField())
   inhale acc(p$c$PrimitiveField$shared(p$pf), wildcard)
-  ret$0 := df$rt$unitValue()
   inhale acc(p$pf.bf$a, write)
   p$pf.bf$a := df$rt$intToRef(0)
   exhale acc(p$pf.bf$a, write)
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /setters.kt:(170,194): info: Generated Viper text for testReferenceFieldSetter:
@@ -32,12 +32,12 @@ method f$testReferenceFieldSetter$TF$T$c$ReferenceField(p$rf: Ref)
   var anon$0: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$rf), df$rt$T$c$ReferenceField())
   inhale acc(p$c$ReferenceField$shared(p$rf), wildcard)
-  ret$0 := df$rt$unitValue()
   anon$0 := con$c$PrimitiveField$T$Int(df$rt$intToRef(0))
   inhale acc(p$rf.bf$pf, write)
   p$rf.bf$pf := anon$0
   exhale acc(p$rf.bf$pf, write)
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /setters.kt:(427,454): info: Generated Viper text for testPrimitivePropertySetter:
@@ -48,9 +48,9 @@ method f$testPrimitivePropertySetter$TF$T$c$PrimitiveProperty(p$pp: Ref)
   var anon$0: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$pp), df$rt$T$c$PrimitiveProperty())
   inhale acc(p$c$PrimitiveProperty$shared(p$pp), wildcard)
-  ret$0 := df$rt$unitValue()
   anon$0 := ps$public$aProp(p$pp, df$rt$intToRef(0))
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method pg$public$aProp(this: Ref) returns (ret: Ref)
@@ -74,10 +74,10 @@ method f$testReferencePropertySetter$TF$T$c$ReferenceProperty(p$rp: Ref)
   var anon$1: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$rp), df$rt$T$c$ReferenceProperty())
   inhale acc(p$c$ReferenceProperty$shared(p$rp), wildcard)
-  ret$0 := df$rt$unitValue()
   anon$1 := con$c$PrimitiveProperty$()
   anon$0 := ps$public$ppProp(p$rp, anon$1)
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method pg$public$aProp(this: Ref) returns (ret: Ref)
@@ -90,4 +90,3 @@ method ps$public$aProp(this: Ref, anon$0: Ref) returns (ret: Ref)
 
 
 method ps$public$ppProp(this: Ref, anon$0: Ref) returns (ret: Ref)
-
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/subtyping.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/subtyping.fir.diag.txt
index 93b727042bb77..c54f65637022a 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/subtyping.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/subtyping.fir.diag.txt
@@ -27,10 +27,10 @@ method f$assignmentSubtyping$TF$() returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   var l0$x: Ref
-  ret$0 := df$rt$unitValue()
   l0$x := df$rt$boolToRef(false)
   l0$x := df$rt$boolToRef(true)
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /subtyping.kt:(358,384): info: Generated Viper text for functionParameterSubtyping:
@@ -38,9 +38,9 @@ method f$functionParameterSubtyping$TF$() returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   var anon$0: Ref
-  ret$0 := df$rt$unitValue()
   anon$0 := f$nullableParameter$TF$Boolean(df$rt$boolToRef(false))
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method f$nullableParameter$TF$Boolean(p$b: Ref) returns (ret: Ref)
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/unique_predicates.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/unique_predicates.fir.diag.txt
index 4c563a6d956f4..244b3413eaacb 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/classes/unique_predicates.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/classes/unique_predicates.fir.diag.txt
@@ -54,8 +54,8 @@ method f$unique_foo_arg$TF$T$c$Foo(p$foo: Ref) returns (ret$0: Ref)
 {
   inhale df$rt$isSubtype(df$rt$typeOf(p$foo), df$rt$T$c$Foo())
   inhale acc(p$c$Foo$shared(p$foo), wildcard)
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /unique_predicates.kt:(310,329): info: Generated Viper text for nullable_unique_arg:
@@ -73,8 +73,8 @@ method f$nullable_unique_arg$TF$c$T(p$t: Ref) returns (ret$0: Ref)
 {
   inhale df$rt$isSubtype(df$rt$typeOf(p$t), df$rt$nullable(df$rt$T$c$T()))
   inhale p$t != df$rt$nullValue() ==> acc(p$c$T$shared(p$t), wildcard)
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /unique_predicates.kt:(353,372): info: Generated Viper text for borrowed_unique_arg:
@@ -93,8 +93,8 @@ method f$borrowed_unique_arg$TF$T$c$T(p$t: Ref) returns (ret$0: Ref)
 {
   inhale df$rt$isSubtype(df$rt$typeOf(p$t), df$rt$T$c$T())
   inhale acc(p$c$T$shared(p$t), wildcard)
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /unique_predicates.kt:(424,439): info: Generated Viper text for unique_receiver:
@@ -112,8 +112,8 @@ method f$unique_receiver$TF$T$c$T(this: Ref) returns (ret$0: Ref)
 {
   inhale df$rt$isSubtype(df$rt$typeOf(this), df$rt$T$c$T())
   inhale acc(p$c$T$shared(this), wildcard)
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /unique_predicates.kt:(488,512): info: Generated Viper text for borrowed_unique_receiver:
@@ -132,8 +132,8 @@ method f$borrowed_unique_receiver$TF$T$c$T(this: Ref) returns (ret$0: Ref)
 {
   inhale df$rt$isSubtype(df$rt$typeOf(this), df$rt$T$c$T())
   inhale acc(p$c$T$shared(this), wildcard)
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /unique_predicates.kt:(531,544): info: Generated Viper text for unique_result:
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/exp_side_effects.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/exp_side_effects.fir.diag.txt
index 82b46072a1eae..b59c9aee9f190 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/exp_side_effects.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/exp_side_effects.fir.diag.txt
@@ -19,7 +19,6 @@ method f$test$TF$() returns (ret$0: Ref)
   var anon$2: Ref
   var anon$3: Ref
   var anon$4: Ref
-  ret$0 := df$rt$unitValue()
   anon$0 := f$getFoo$TF$()
   anon$1 := f$sideEffect$TF$()
   inhale acc(anon$0.bf$x, write)
@@ -33,4 +32,5 @@ method f$test$TF$() returns (ret$0: Ref)
   anon$4 := f$sideEffect$TF$()
   l0$y := sp$plusInts(anon$2, anon$4)
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/function_call.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/function_call.fir.diag.txt
index 0b2aeb17a33c5..2c778d1665957 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/function_call.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/function_call.fir.diag.txt
@@ -8,10 +8,10 @@ method f$functionCall$TF$() returns (ret$0: Ref)
 {
   var anon$0: Ref
   var anon$1: Ref
-  ret$0 := df$rt$unitValue()
   anon$0 := f$f$TF$T$Int(df$rt$intToRef(0))
   anon$1 := f$f$TF$T$Int(df$rt$intToRef(0))
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /function_call.kt:(160,178): info: Generated Viper text for functionCallNested:
@@ -25,9 +25,9 @@ method f$functionCallNested$TF$() returns (ret$0: Ref)
   var anon$0: Ref
   var anon$1: Ref
   var anon$2: Ref
-  ret$0 := df$rt$unitValue()
   anon$2 := f$f$TF$T$Int(df$rt$intToRef(0))
   anon$1 := f$f$TF$T$Int(anon$2)
   anon$0 := f$f$TF$T$Int(anon$1)
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/loop.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/loop.fir.diag.txt
index bab27d9692844..b747426cc51a3 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/loop.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/loop.fir.diag.txt
@@ -26,7 +26,6 @@ method f$whileFunctionCondition$TF$() returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   var anon$0: Ref
-  ret$0 := df$rt$unitValue()
   label lbl$continue$0
   anon$0 := f$whileLoop$TF$T$Boolean(df$rt$boolToRef(true))
   while (df$rt$boolFromRef(anon$0))
@@ -36,6 +35,7 @@ method f$whileFunctionCondition$TF$() returns (ret$0: Ref)
   }
   label lbl$break$0
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method f$whileLoop$TF$T$Boolean(p$b: Ref) returns (ret: Ref)
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/loop_invariants.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/loop_invariants.fir.diag.txt
index 034c27c9ddac6..b7207bff161d0 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/loop_invariants.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/loop_invariants.fir.diag.txt
@@ -4,7 +4,6 @@ method f$dynamicLambdaInvariant$TF$TF$(p$f: Ref) returns (ret$0: Ref)
 {
   var anon$0: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$f), df$rt$functionType())
-  ret$0 := df$rt$unitValue()
   label lbl$continue$0
   anon$0 := f$returnsBoolean$TF$()
   while (df$rt$boolFromRef(anon$0))
@@ -16,6 +15,7 @@ method f$dynamicLambdaInvariant$TF$TF$(p$f: Ref) returns (ret$0: Ref)
   }
   label lbl$break$0
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method f$returnsBoolean$TF$() returns (ret: Ref)
@@ -29,7 +29,6 @@ method f$functionAssignment$TF$TF$(p$f: Ref) returns (ret$0: Ref)
   var l0$g: Ref
   var anon$0: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$f), df$rt$functionType())
-  ret$0 := df$rt$unitValue()
   l0$g := p$f
   label lbl$continue$0
   anon$0 := f$returnsBoolean$TF$()
@@ -42,6 +41,7 @@ method f$functionAssignment$TF$TF$(p$f: Ref) returns (ret$0: Ref)
   }
   label lbl$break$0
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method f$returnsBoolean$TF$() returns (ret: Ref)
@@ -59,7 +59,6 @@ method f$conditionalFunctionAssignment$TF$T$Boolean$TF$$TF$(p$b: Ref, p$f: Ref,
   inhale df$rt$isSubtype(df$rt$typeOf(p$b), df$rt$boolType())
   inhale df$rt$isSubtype(df$rt$typeOf(p$f), df$rt$functionType())
   inhale df$rt$isSubtype(df$rt$typeOf(p$h), df$rt$functionType())
-  ret$0 := df$rt$unitValue()
   if (df$rt$boolFromRef(p$b)) {
     l0$g := p$f
   } else {
@@ -75,6 +74,7 @@ method f$conditionalFunctionAssignment$TF$T$Boolean$TF$$TF$(p$b: Ref, p$f: Ref,
   }
   label lbl$break$0
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method f$returnsBoolean$TF$() returns (ret: Ref)
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/recursion.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/recursion.fir.diag.txt
index 37284f44ab17b..22872b7b2e680 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/recursion.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/recursion.fir.diag.txt
@@ -2,8 +2,8 @@
 method f$recursive$TF$() returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
-  ret$0 := df$rt$unitValue()
   ret$0 := f$recursive$TF$()
   goto lbl$ret$0
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/return_break_continue.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/return_break_continue.fir.diag.txt
index 1add7c7943a74..93a86f10159ca 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/return_break_continue.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/return_break_continue.fir.diag.txt
@@ -58,7 +58,6 @@ method f$whileContinue$TF$() returns (ret$0: Ref)
 {
   var l0$b: Ref
   var anon$0: Ref
-  ret$0 := df$rt$unitValue()
   l0$b := df$rt$boolToRef(true)
   label lbl$continue$0
   anon$0 := l0$b
@@ -71,6 +70,7 @@ method f$whileContinue$TF$() returns (ret$0: Ref)
   }
   label lbl$break$0
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /return_break_continue.kt:(375,386): info: Generated Viper text for whileNested:
@@ -79,7 +79,6 @@ method f$whileNested$TF$T$Boolean(p$b: Ref) returns (ret$0: Ref)
 {
   var anon$0: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$b), df$rt$boolType())
-  ret$0 := df$rt$unitValue()
   label lbl$continue$0
   anon$0 := p$b
   while (df$rt$boolFromRef(anon$0))
@@ -111,6 +110,7 @@ method f$whileNested$TF$T$Boolean(p$b: Ref) returns (ret$0: Ref)
   }
   label lbl$break$0
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /return_break_continue.kt:(556,569): info: Generated Viper text for labelledBreak:
@@ -119,7 +119,6 @@ method f$labelledBreak$TF$T$Boolean(p$b: Ref) returns (ret$0: Ref)
 {
   var anon$0: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$b), df$rt$boolType())
-  ret$0 := df$rt$unitValue()
   label lbl$continue$0
   anon$0 := p$b
   while (df$rt$boolFromRef(anon$0))
@@ -143,6 +142,7 @@ method f$labelledBreak$TF$T$Boolean(p$b: Ref) returns (ret$0: Ref)
   }
   label lbl$break$0
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /return_break_continue.kt:(754,770): info: Generated Viper text for labelledContinue:
@@ -151,7 +151,6 @@ method f$labelledContinue$TF$T$Boolean(p$b: Ref) returns (ret$0: Ref)
 {
   var anon$0: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$b), df$rt$boolType())
-  ret$0 := df$rt$unitValue()
   label lbl$continue$0
   anon$0 := p$b
   while (df$rt$boolFromRef(anon$0))
@@ -175,6 +174,7 @@ method f$labelledContinue$TF$T$Boolean(p$b: Ref) returns (ret$0: Ref)
   }
   label lbl$break$0
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /return_break_continue.kt:(970,992): info: Generated Viper text for labelledWhileShadowing:
@@ -183,7 +183,6 @@ method f$labelledWhileShadowing$TF$T$Boolean(p$b: Ref) returns (ret$0: Ref)
 {
   var anon$0: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$b), df$rt$boolType())
-  ret$0 := df$rt$unitValue()
   label lbl$continue$0
   anon$0 := p$b
   while (df$rt$boolFromRef(anon$0))
@@ -217,4 +216,5 @@ method f$labelledWhileShadowing$TF$T$Boolean(p$b: Ref) returns (ret$0: Ref)
   }
   label lbl$break$0
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/try_catch.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/try_catch.fir.diag.txt
index c4706a0f1effd..b57bd4caeecda 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/try_catch.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/try_catch.fir.diag.txt
@@ -12,7 +12,6 @@ method f$tryCatch$TF$() returns (ret$0: Ref)
   var anon$3: Ref
   var l2$e: Ref
   var anon$4: Ref
-  ret$0 := df$rt$unitValue()
   if (df$rt$boolFromRef(anon$0)) {
     goto lbl$catch$0
   }
@@ -27,6 +26,7 @@ method f$tryCatch$TF$() returns (ret$0: Ref)
   goto lbl$try_exit$0
   label lbl$try_exit$0
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method pg$public$cause(this: Ref) returns (ret: Ref)
@@ -52,7 +52,6 @@ method f$nestedTryCatch$TF$() returns (ret$0: Ref)
   var anon$5: Ref
   var anon$6: Ref
   var l4$e: Ref
-  ret$0 := df$rt$unitValue()
   if (df$rt$boolFromRef(anon$0)) {
     goto lbl$catch$0
   }
@@ -77,6 +76,7 @@ method f$nestedTryCatch$TF$() returns (ret$0: Ref)
   goto lbl$try_exit$0
   label lbl$try_exit$0
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method pg$public$cause(this: Ref) returns (ret: Ref)
@@ -100,13 +100,13 @@ method f$tryCatchWithInline$TF$() returns (ret$0: Ref)
   var anon$3: Ref
   var l3$e: Ref
   var anon$4: Ref
-  ret$0 := df$rt$unitValue()
   if (df$rt$boolFromRef(anon$0)) {
     goto lbl$catch$0
   }
   anon$1 := f$call$TF$T$Int(df$rt$intToRef(0))
   anon$2 := f$call$TF$T$Int(df$rt$intToRef(1))
   label lbl$ret$1
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$1), df$rt$unitType())
   if (df$rt$boolFromRef(anon$3)) {
     goto lbl$catch$0
   }
@@ -116,6 +116,7 @@ method f$tryCatchWithInline$TF$() returns (ret$0: Ref)
   goto lbl$try_exit$0
   label lbl$try_exit$0
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method pg$public$cause(this: Ref) returns (ret: Ref)
@@ -134,7 +135,6 @@ method f$tryCatchShadowing$TF$() returns (ret$0: Ref)
   var anon$1: Ref
   var l2$e: Ref
   var l2$x: Ref
-  ret$0 := df$rt$unitValue()
   l0$x := df$rt$intToRef(0)
   if (df$rt$boolFromRef(anon$0)) {
     goto lbl$catch$0
@@ -149,6 +149,7 @@ method f$tryCatchShadowing$TF$() returns (ret$0: Ref)
   goto lbl$try_exit$0
   label lbl$try_exit$0
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method pg$public$cause(this: Ref) returns (ret: Ref)
@@ -175,7 +176,6 @@ method f$multipleCatches$TF$() returns (ret$0: Ref)
   var anon$6: Ref
   var l3$e: Ref
   var anon$7: Ref
-  ret$0 := df$rt$unitValue()
   if (df$rt$boolFromRef(anon$0)) {
     goto lbl$catch$0
   }
@@ -199,6 +199,7 @@ method f$multipleCatches$TF$() returns (ret$0: Ref)
   goto lbl$try_exit$0
   label lbl$try_exit$0
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method pg$public$cause(this: Ref) returns (ret: Ref)
@@ -224,7 +225,6 @@ method f$useException$TF$() returns (ret$0: Ref)
   var anon$2: Ref
   var l2$e: Ref
   var anon$3: Ref
-  ret$0 := df$rt$unitValue()
   if (df$rt$boolFromRef(anon$0)) {
     goto lbl$catch$0
   }
@@ -238,6 +238,7 @@ method f$useException$TF$() returns (ret$0: Ref)
   goto lbl$try_exit$0
   label lbl$try_exit$0
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method pg$public$cause(this: Ref) returns (ret: Ref)
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/when.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/when.fir.diag.txt
index 24a5c0d4f99aa..ff7e052d3c427 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/when.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/when.fir.diag.txt
@@ -180,7 +180,6 @@ method f$whenSubjectValNested$TF$() returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   var l1$x: Ref
-  ret$0 := df$rt$unitValue()
   l1$x := df$rt$intToRef(1)
   if (df$rt$intFromRef(l1$x) == 0) {
   } else {
@@ -203,6 +202,7 @@ method f$whenSubjectValNested$TF$() returns (ret$0: Ref)
     }
   }
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /when.kt:(1674,1697): info: Generated Viper text for whenSubjectVarShadowing:
@@ -211,8 +211,8 @@ method f$whenSubjectVarShadowing$TF$() returns (ret$0: Ref)
 {
   var l0$x: Ref
   var l1$x: Ref
-  ret$0 := df$rt$unitValue()
   l0$x := df$rt$intToRef(0)
   l1$x := df$rt$intToRef(1)
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/extension_properties.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/extension_properties.fir.diag.txt
index 14e926e80e506..ba474ffb3c98e 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/extension_properties.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/extension_properties.fir.diag.txt
@@ -11,7 +11,6 @@ method f$extensionGetterProperty$TF$() returns (ret$0: Ref)
   var anon$1: Ref
   var anon$2: Ref
   var anon$3: Ref
-  ret$0 := df$rt$unitValue()
   anon$0 := eg$intValProp$TF$T$Int(df$rt$intToRef(0))
   l0$a := anon$0
   inhale df$rt$isSubtype(df$rt$typeOf(l0$a), df$rt$intType())
@@ -22,6 +21,7 @@ method f$extensionGetterProperty$TF$() returns (ret$0: Ref)
   l0$b := anon$1
   inhale df$rt$isSubtype(df$rt$typeOf(l0$b), df$rt$intType())
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /extension_properties.kt:(210,233): info: Generated Viper text for extensionSetterProperty:
@@ -36,9 +36,9 @@ method f$extensionSetterProperty$TF$() returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   var anon$0: Ref
-  ret$0 := df$rt$unitValue()
   anon$0 := es$intVarProp$TF$T$Int$T$Int(df$rt$intToRef(42), df$rt$intToRef(0))
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /extension_properties.kt:(414,453): info: Generated Viper text for extensionGetterPropertyUserDefinedClass:
@@ -55,11 +55,11 @@ method f$extensionGetterPropertyUserDefinedClass$TF$T$c$PrimitiveField(p$pf: Ref
   var anon$0: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$pf), df$rt$T$c$PrimitiveField())
   inhale acc(p$c$PrimitiveField$shared(p$pf), wildcard)
-  ret$0 := df$rt$unitValue()
   anon$0 := eg$pfValProp$TF$T$c$PrimitiveField(p$pf)
   l0$x := anon$0
   inhale df$rt$isSubtype(df$rt$typeOf(l0$x), df$rt$intType())
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /extension_properties.kt:(508,547): info: Generated Viper text for extensionSetterPropertyUserDefinedClass:
@@ -79,7 +79,7 @@ method f$extensionSetterPropertyUserDefinedClass$TF$T$c$PrimitiveField(p$pf: Ref
   var anon$0: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$pf), df$rt$T$c$PrimitiveField())
   inhale acc(p$c$PrimitiveField$shared(p$pf), wildcard)
-  ret$0 := df$rt$unitValue()
   anon$0 := es$pfVarProp$TF$T$c$PrimitiveField$T$Int(p$pf, df$rt$intToRef(42))
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/full_viper_dump.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/full_viper_dump.fir.diag.txt
index a74a8b29eae16..de3a35d69d9fe 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/full_viper_dump.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/full_viper_dump.fir.diag.txt
@@ -291,14 +291,14 @@ method f$f$TF$() returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   var l0$foo: Ref
-  ret$0 := df$rt$unitValue()
   l0$foo := con$c$Foo$T$Int(df$rt$intToRef(0))
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /full_viper_dump.kt:(172,173): info: Generated ExpEmbedding for f$f$TF$:
 Function(
     name = f$f$TF$,
-    { Var(ret$0) := Unit; Declare(Var(l0$foo), T$c$Foo, MethodCall(callee = con$c$Foo$T$Int, Int(0))) },
+    { Declare(Var(l0$foo), T$c$Foo, MethodCall(callee = con$c$Foo$T$Int, Int(0))) },
     return = lbl$ret$0,
 )
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/function_object.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/function_object.fir.diag.txt
index fcf3c6bf77480..276d4fac0a437 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/function_object.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/function_object.fir.diag.txt
@@ -3,8 +3,8 @@ method f$unitFunction$TF$TF$(p$f: Ref) returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   inhale df$rt$isSubtype(df$rt$typeOf(p$f), df$rt$functionType())
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /function_object.kt:(90,108): info: Generated Viper text for functionObjectCall:
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/function_overloading.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/function_overloading.fir.diag.txt
index 72bd716958a35..cc437d57e441a 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/function_overloading.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/function_overloading.fir.diag.txt
@@ -7,8 +7,8 @@ method f$c$Bar$baz$TF$T$c$Bar$T$c$Foo(this: Ref, p$f: Ref)
   inhale acc(p$c$Bar$shared(this), wildcard)
   inhale df$rt$isSubtype(df$rt$typeOf(p$f), df$rt$T$c$Foo())
   inhale acc(p$c$Foo$shared(p$f), wildcard)
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /function_overloading.kt:(74,77): info: Generated Viper text for baz:
@@ -20,8 +20,8 @@ method f$c$Bar$baz$TF$T$c$Bar$T$c$Bar(this: Ref, p$b: Ref)
   inhale acc(p$c$Bar$shared(this), wildcard)
   inhale df$rt$isSubtype(df$rt$typeOf(p$b), df$rt$T$c$Bar())
   inhale acc(p$c$Bar$shared(p$b), wildcard)
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /function_overloading.kt:(98,107): info: Generated Viper text for fakePrint:
@@ -30,8 +30,8 @@ method f$fakePrint$TF$T$c$Bar(p$b: Ref) returns (ret$0: Ref)
 {
   inhale df$rt$isSubtype(df$rt$typeOf(p$b), df$rt$T$c$Bar())
   inhale acc(p$c$Bar$shared(p$b), wildcard)
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /function_overloading.kt:(125,134): info: Generated Viper text for fakePrint:
@@ -40,8 +40,8 @@ method f$fakePrint$TF$T$c$Foo(p$f: Ref) returns (ret$0: Ref)
 {
   inhale df$rt$isSubtype(df$rt$typeOf(p$f), df$rt$T$c$Foo())
   inhale acc(p$c$Foo$shared(p$f), wildcard)
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /function_overloading.kt:(152,161): info: Generated Viper text for fakePrint:
@@ -49,8 +49,8 @@ method f$fakePrint$TF$T$Int(p$value: Ref) returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   inhale df$rt$isSubtype(df$rt$typeOf(p$value), df$rt$intType())
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /function_overloading.kt:(183,192): info: Generated Viper text for fakePrint:
@@ -58,8 +58,8 @@ method f$fakePrint$TF$T$Boolean(p$truth: Ref) returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   inhale df$rt$isSubtype(df$rt$typeOf(p$truth), df$rt$boolType())
-  ret$0 := df$rt$unitValue()
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /function_overloading.kt:(219,245): info: Generated Viper text for testGlobalScopeOverloading:
@@ -100,7 +100,6 @@ method f$testGlobalScopeOverloading$TF$() returns (ret$0: Ref)
   var anon$3: Ref
   var anon$4: Ref
   var anon$5: Ref
-  ret$0 := df$rt$unitValue()
   anon$0 := f$fakePrint$TF$T$Int(df$rt$intToRef(42))
   anon$1 := f$fakePrint$TF$T$Boolean(df$rt$boolToRef(true))
   anon$3 := con$c$Foo$()
@@ -108,6 +107,7 @@ method f$testGlobalScopeOverloading$TF$() returns (ret$0: Ref)
   anon$5 := con$c$Bar$()
   anon$4 := f$fakePrint$TF$T$c$Bar(anon$5)
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /function_overloading.kt:(337,365): info: Generated Viper text for testClassFunctionOverloading:
@@ -141,11 +141,11 @@ method f$testClassFunctionOverloading$TF$() returns (ret$0: Ref)
   var anon$1: Ref
   var anon$2: Ref
   var anon$3: Ref
-  ret$0 := df$rt$unitValue()
   l0$b := con$c$Bar$()
   anon$1 := con$c$Foo$()
   anon$0 := f$c$Bar$baz$TF$T$c$Bar$T$c$Foo(l0$b, anon$1)
   anon$3 := con$c$Bar$()
   anon$2 := f$c$Bar$baz$TF$T$c$Bar$T$c$Bar(l0$b, anon$3)
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/inlining/lambdas.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/inlining/lambdas.fir.diag.txt
index 529fd996832ab..c65ae783af693 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/inlining/lambdas.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/inlining/lambdas.fir.diag.txt
@@ -65,7 +65,6 @@ method f$returnValueNotUsed$TF$() returns (ret$0: Ref)
   var ret$1: Ref
   var ret$2: Ref
   var anon$0: Ref
-  ret$0 := df$rt$unitValue()
   anon$0 := df$rt$intToRef(0)
   ret$2 := anon$0
   goto lbl$ret$2
@@ -74,6 +73,7 @@ method f$returnValueNotUsed$TF$() returns (ret$0: Ref)
   goto lbl$ret$1
   label lbl$ret$1
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /lambdas.kt:(466,475): info: Generated Viper text for shadowing:
@@ -136,7 +136,6 @@ method f$lambdaPassthrough$TF$() returns (ret$0: Ref)
   var ret$2: Ref
   var ret$3: Ref
   var anon$0: Ref
-  ret$0 := df$rt$unitValue()
   anon$0 := df$rt$intToRef(0)
   ret$3 := sp$plusInts(anon$0, df$rt$intToRef(1))
   goto lbl$ret$3
@@ -145,5 +144,7 @@ method f$lambdaPassthrough$TF$() returns (ret$0: Ref)
   goto lbl$ret$2
   label lbl$ret$2
   label lbl$ret$1
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$1), 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/no_contracts/operators/arithmetic.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/operators/arithmetic.fir.diag.txt
index 11e025266cd96..1e2034c71cba4 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/operators/arithmetic.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/operators/arithmetic.fir.diag.txt
@@ -4,9 +4,9 @@ method f$addition$TF$T$Int(p$x: Ref) returns (ret$0: Ref)
 {
   var l0$y: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$intType())
-  ret$0 := df$rt$unitValue()
   l0$y := sp$plusInts(p$x, p$x)
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /arithmetic.kt:(66,77): info: Generated Viper text for subtraction:
@@ -15,9 +15,9 @@ method f$subtraction$TF$T$Int(p$x: Ref) returns (ret$0: Ref)
 {
   var l0$y: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$intType())
-  ret$0 := df$rt$unitValue()
   l0$y := sp$minusInts(p$x, p$x)
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /arithmetic.kt:(112,126): info: Generated Viper text for multiplication:
@@ -26,9 +26,9 @@ method f$multiplication$TF$T$Int(p$x: Ref) returns (ret$0: Ref)
 {
   var l0$y: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$intType())
-  ret$0 := df$rt$unitValue()
   l0$y := sp$timesInts(p$x, p$x)
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /arithmetic.kt:(161,169): info: Generated Viper text for division:
@@ -37,8 +37,8 @@ method f$division$TF$T$Int(p$x: Ref) returns (ret$0: Ref)
 {
   var l0$y: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$intType())
-  ret$0 := df$rt$unitValue()
   inhale df$rt$intFromRef(p$x) != 0
   l0$y := sp$divInts(p$x, p$x)
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/shadowing.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/shadowing.fir.diag.txt
index 58a040bc3359b..44ce33cb105a5 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/shadowing.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/shadowing.fir.diag.txt
@@ -4,7 +4,6 @@ method f$shadowLocal$TF$() returns (ret$0: Ref)
 {
   var l0$foo: Ref
   var l0$x: Ref
-  ret$0 := df$rt$unitValue()
   l0$x := df$rt$intToRef(0)
   if (df$rt$intFromRef(l0$x) == 0) {
     var l2$x: Ref
@@ -19,6 +18,7 @@ method f$shadowLocal$TF$() returns (ret$0: Ref)
   }
   l0$foo := l0$x
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /shadowing.kt:(232,243): info: Generated Viper text for shadowParam:
@@ -28,11 +28,11 @@ method f$shadowParam$TF$T$Int(p$x: Ref) returns (ret$0: Ref)
   var l0$foo: Ref
   var l0$x: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$intType())
-  ret$0 := df$rt$unitValue()
   l0$foo := p$x
   l0$x := df$rt$intToRef(0)
   l0$foo := l0$x
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /shadowing.kt:(322,334): info: Generated Viper text for shadowNested:
@@ -42,7 +42,6 @@ method f$shadowNested$TF$T$Int(p$x: Ref) returns (ret$0: Ref)
   var l0$foo: Ref
   var l0$x: Ref
   inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$intType())
-  ret$0 := df$rt$unitValue()
   l0$foo := p$x
   l0$x := df$rt$intToRef(0)
   l0$foo := l0$x
@@ -68,4 +67,5 @@ method f$shadowNested$TF$T$Int(p$x: Ref) returns (ret$0: Ref)
   }
   l0$foo := l0$x
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/types/generics.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/types/generics.fir.diag.txt
index 8a4693fca2a88..a0c2ad1f3fd9f 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/types/generics.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/types/generics.fir.diag.txt
@@ -61,12 +61,12 @@ method f$setGenericField$TF$() returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   var l0$box: Ref
-  ret$0 := df$rt$unitValue()
   l0$box := con$c$Box$Any(df$rt$intToRef(3))
   inhale acc(l0$box.bf$t, write)
   l0$box.bf$t := df$rt$intToRef(5)
   exhale acc(l0$box.bf$t, write)
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 /generics.kt:(293,303): info: Generated Viper text for genericFun:
@@ -85,10 +85,11 @@ method f$callGenericFunc$TF$() returns (ret$0: Ref)
 {
   var l0$x: Ref
   var anon$0: Ref
-  ret$0 := df$rt$unitValue()
   anon$0 := f$genericFun$TF$Any(df$rt$intToRef(3))
   l0$x := anon$0
+  inhale df$rt$isSubtype(df$rt$typeOf(l0$x), df$rt$intType())
   label lbl$ret$0
+  inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
 method f$genericFun$TF$Any(p$t: Ref) returns (ret: Ref)
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 4854b9eec27b5..55c713bf60c22 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
@@ -192,6 +192,18 @@ public void testReturns_null() {
     public void testSimple() {
       runTest("plugins/formal-verification/testData/diagnostics/good_contracts/simple.kt");
     }
+
+    @Test
+    @TestMetadata("unit_return_type.kt")
+    public void testUnit_return_type() {
+      runTest("plugins/formal-verification/testData/diagnostics/good_contracts/unit_return_type.kt");
+    }
+
+    @Test
+    @TestMetadata("viper_casts_while_inlining.kt")
+    public void testViper_casts_while_inlining() {
+      runTest("plugins/formal-verification/testData/diagnostics/good_contracts/viper_casts_while_inlining.kt");
+    }
   }
 
   @Nested