tests regenerated

plugins/formal-verification/testData/diagnostics/bad_contracts/cond_effects.fir.diag.txt

@@ -12,7 +12,7 @@ method f$compoundConditionalEffect$TF$T$Boolean(p$b: Ref)
 /cond_effects.kt:(190,220): warning: Cannot verify that if the function returns then (b && false).
 
 /cond_effects.kt:(271,287): info: Generated Viper text for mayReturnNonNull:
-method f$mayReturnNonNull$TF$T$N$Any(p$x: Ref) returns (ret$0: Ref)
+method f$mayReturnNonNull$TF$N$Any(p$x: Ref) returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$nullable(df$rt$anyType()))
   ensures ret$0 == df$rt$nullValue() ==>
     df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$intType())
@@ -26,7 +26,7 @@ method f$mayReturnNonNull$TF$T$N$Any(p$x: Ref) returns (ret$0: Ref)
 /cond_effects.kt:(328,360): warning: Cannot verify that if a null value is returned then x is Int.
 
 /cond_effects.kt:(424,437): info: Generated Viper text for mayReturnNull:
-method f$mayReturnNull$TF$T$N$Any(p$x: Ref) returns (ret$0: Ref)
+method f$mayReturnNull$TF$N$Any(p$x: Ref) returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$nullable(df$rt$anyType()))
   ensures ret$0 != df$rt$nullValue() ==>
     df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$intType())
@@ -40,7 +40,7 @@ method f$mayReturnNull$TF$T$N$Any(p$x: Ref) returns (ret$0: Ref)
 /cond_effects.kt:(478,513): warning: Cannot verify that if a non-null value is returned then x is Int.
 
 /cond_effects.kt:(723,741): info: Generated Viper text for isNullOrEmptyWrong:
-method f$isNullOrEmptyWrong$TF$T$N$c$pkg$kotlin$CharSequence(p$seq: Ref)
+method f$isNullOrEmptyWrong$TF$N$c$pkg$kotlin$CharSequence(p$seq: Ref)
   returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$boolType())
   ensures df$rt$boolFromRef(ret$0) == false ==> p$seq != df$rt$nullValue()
@@ -69,7 +69,7 @@ method pg$public$length(this$dispatch: Ref) returns (ret: Ref)
 /cond_effects.kt:(925,942): info: Generated Viper text for recursiveContract:
 field bf$length: Ref
 
-method f$recursiveContract$TF$T$Int$T$N$Any(p$n: Ref, p$x: Ref)
+method f$recursiveContract$TF$T$Int$N$Any(p$n: Ref, p$x: Ref)
   returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$boolType())
   ensures df$rt$boolFromRef(ret$0) == true ==>
@@ -80,7 +80,7 @@ method f$recursiveContract$TF$T$Int$T$N$Any(p$n: Ref, p$x: Ref)
   if (df$rt$intFromRef(p$n) == 0) {
     ret$0 := df$rt$boolToRef(df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$intType()))
   } else {
-    ret$0 := f$recursiveContract$TF$T$Int$T$N$Any(sp$minusInts(p$n, df$rt$intToRef(1)),
+    ret$0 := f$recursiveContract$TF$T$Int$N$Any(sp$minusInts(p$n, df$rt$intToRef(1)),
       p$x)}
   goto lbl$ret$0
   label lbl$ret$0

plugins/formal-verification/testData/diagnostics/bad_contracts/is_type_contract.fir.diag.txt

@@ -1,7 +1,7 @@
 /is_type_contract.kt:(151,172): info: Generated Viper text for unverifiableTypeCheck:
 field bf$length: Ref
 
-method f$unverifiableTypeCheck$TF$T$N$Int(p$x: Ref) returns (ret$0: Ref)
+method f$unverifiableTypeCheck$TF$N$Int(p$x: Ref) returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$boolType())
   ensures true ==> df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$unitType())
 {
@@ -17,7 +17,7 @@ method pg$public$length(this$dispatch: Ref) returns (ret: Ref)
 /is_type_contract.kt:(216,245): warning: Cannot verify that if the function returns then x is Unit.
 
 /is_type_contract.kt:(319,341): info: Generated Viper text for nullableNotNonNullable:
-method f$nullableNotNonNullable$TF$T$N$Int(p$x: Ref) returns (ret$0: Ref)
+method f$nullableNotNonNullable$TF$N$Int(p$x: Ref) returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
   ensures true ==> df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$intType())
 {

plugins/formal-verification/testData/diagnostics/bad_contracts/returns_null.fir.diag.txt

@@ -1,6 +1,5 @@
 /returns_null.kt:(121,146): info: Generated Viper text for returns_null_unverifiable:
-method f$returns_null_unverifiable$TF$T$N$Int(p$x: Ref)
-  returns (ret$0: Ref)
+method f$returns_null_unverifiable$TF$N$Int(p$x: Ref) returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$nullable(df$rt$intType()))
   ensures true ==> false
 {

plugins/formal-verification/testData/diagnostics/good_contracts/backing_field_getters.fir.diag.txt

@@ -24,7 +24,7 @@ field bf$y: Ref
 
 field bf$z: Ref
 
-method f$receiverNotNullProved$TF$T$N$c$X(p$x: Ref) returns (ret$0: Ref)
+method f$receiverNotNullProved$TF$N$c$X(p$x: Ref) returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$boolType())
   ensures df$rt$boolFromRef(ret$0) == true ==> p$x != df$rt$nullValue()
 {
@@ -48,8 +48,7 @@ field bf$y: Ref
 
 field bf$z: Ref
 
-method f$cascadeNullableGet$TF$T$N$c$NullableX(p$x: Ref)
-  returns (ret$0: Ref)
+method f$cascadeNullableGet$TF$N$c$NullableX(p$x: Ref) returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$nullable(df$rt$T$c$Z()))
   ensures ret$0 != df$rt$nullValue() ==> acc(p$c$Z$shared(ret$0), wildcard)
   ensures ret$0 != df$rt$nullValue() ==> p$x != df$rt$nullValue()
@@ -77,7 +76,7 @@ field bf$y: Ref
 
 field bf$z: Ref
 
-method f$cascadeNullableSmartcastGet$TF$T$N$c$NullableX(p$x: Ref)
+method f$cascadeNullableSmartcastGet$TF$N$c$NullableX(p$x: Ref)
   returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$nullable(df$rt$T$c$Z()))
   ensures ret$0 != df$rt$nullValue() ==> acc(p$c$Z$shared(ret$0), wildcard)

plugins/formal-verification/testData/diagnostics/good_contracts/is_type_contract.fir.diag.txt

@@ -1,7 +1,7 @@
 /is_type_contract.kt:(157,165): info: Generated Viper text for isString:
 field bf$length: Ref
 
-method f$isString$TF$T$N$Any(p$x: Ref) returns (ret$0: Ref)
+method f$isString$TF$N$Any(p$x: Ref) returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$boolType())
   ensures df$rt$boolFromRef(ret$0) == true ==>
     df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$T$c$pkg$kotlin$String())

plugins/formal-verification/testData/diagnostics/good_contracts/list.fir.diag.txt

@@ -191,7 +191,7 @@ method f$pkg$kotlin_collections$c$List$isEmpty$TF$T$c$pkg$kotlin_collections$Lis
 /list.kt:(670,683): info: Generated Viper text for nullable_list:
 field sp$size: Ref
 
-method f$nullable_list$TF$T$N$c$pkg$kotlin_collections$List(p$l: Ref)
+method f$nullable_list$TF$N$c$pkg$kotlin_collections$List(p$l: Ref)
   returns (ret$0: Ref)
   requires p$l != df$rt$nullValue() ==> acc(p$l.sp$size, write)
   requires p$l != df$rt$nullValue() ==> df$rt$intFromRef(p$l.sp$size) >= 0

plugins/formal-verification/testData/diagnostics/good_contracts/returns_booleans.fir.diag.txt

@@ -88,7 +88,7 @@ method f$call_fun_with_contracts$TF$T$Boolean(p$b: Ref)
 /returns_booleans.kt:(1467,1480): info: Generated Viper text for isNullOrEmpty:
 field sp$size: Ref
 
-method f$isNullOrEmpty$TF$T$N$c$pkg$kotlin_collections$Collection(p$collection: Ref)
+method f$isNullOrEmpty$TF$N$c$pkg$kotlin_collections$Collection(p$collection: Ref)
   returns (ret$0: Ref)
   requires p$collection != df$rt$nullValue() ==>
     acc(p$collection.sp$size, write)

plugins/formal-verification/testData/diagnostics/good_contracts/returns_null.fir.diag.txt

@@ -1,5 +1,5 @@
 /returns_null.kt:(121,140): info: Generated Viper text for simple_returns_null:
-method f$simple_returns_null$TF$T$N$Int(p$x: Ref) returns (ret$0: Ref)
+method f$simple_returns_null$TF$N$Int(p$x: Ref) returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$nullable(df$rt$intType()))
   ensures ret$0 == df$rt$nullValue()
   ensures ret$0 != df$rt$nullValue() ==> false
@@ -11,7 +11,7 @@ method f$simple_returns_null$TF$T$N$Int(p$x: Ref) returns (ret$0: Ref)
 }
 
 /returns_null.kt:(300,320): info: Generated Viper text for returns_null_implies:
-method f$returns_null_implies$TF$T$N$Boolean(p$x: Ref) returns (ret$0: Ref)
+method f$returns_null_implies$TF$N$Boolean(p$x: Ref) returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$nullable(df$rt$boolType()))
   ensures ret$0 == df$rt$nullValue() ==> p$x == df$rt$nullValue()
   ensures ret$0 != df$rt$nullValue() ==> p$x != df$rt$nullValue()
@@ -23,8 +23,7 @@ method f$returns_null_implies$TF$T$N$Boolean(p$x: Ref) returns (ret$0: Ref)
 }
 
 /returns_null.kt:(511,531): info: Generated Viper text for returns_null_with_if:
-method f$returns_null_with_if$TF$T$N$Int$T$N$Int$T$N$Int(p$x: Ref, p$y: Ref,
-  p$z: Ref)
+method f$returns_null_with_if$TF$N$Int$N$Int$N$Int(p$x: Ref, p$y: Ref, p$z: Ref)
   returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$nullable(df$rt$intType()))
   ensures ret$0 == df$rt$nullValue() ==>

plugins/formal-verification/testData/diagnostics/good_contracts/unit_return_type.fir.diag.txt

@@ -1,5 +1,5 @@
 /unit_return_type.kt:(171,176): info: Generated Viper text for idFun:
-method f$idFun$TF$T$N$Any(p$t: Ref) returns (ret$0: Ref)
+method f$idFun$TF$N$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()))
@@ -19,7 +19,7 @@ method f$directReturns$TF$T$Boolean(p$b: Ref) returns (ret$0: Ref)
   } else {
     var anon$0: Ref
     var anon$1: Ref
-    anon$1 := f$idFun$TF$T$N$Any(p$b)
+    anon$1 := f$idFun$TF$N$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)) {
@@ -31,12 +31,12 @@ method f$directReturns$TF$T$Boolean(p$b: Ref) returns (ret$0: Ref)
   inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
-method f$idFun$TF$T$N$Any(p$t: Ref) returns (ret: Ref)
+method f$idFun$TF$N$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$T$N$Any(p$t: Ref) returns (ret: Ref)
+method f$idFun$TF$N$Any(p$t: Ref) returns (ret: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$nullable(df$rt$anyType()))
 
 
@@ -58,7 +58,7 @@ method f$useInlineUnit$TF$T$Boolean(p$b: Ref) returns (ret$0: Ref)
     var anon$2: Ref
     var anon$3: Ref
     l4$tmp := df$rt$intToRef(42)
-    anon$3 := f$idFun$TF$T$N$Any(l4$tmp)
+    anon$3 := f$idFun$TF$N$Any(l4$tmp)
     anon$2 := anon$3
     inhale df$rt$isSubtype(df$rt$typeOf(anon$2), df$rt$intType())
   }

plugins/formal-verification/testData/diagnostics/good_contracts/viper_casts_while_inlining.fir.diag.txt

@@ -1,5 +1,5 @@
 /viper_casts_while_inlining.kt:(250,255): info: Generated Viper text for idFun:
-method f$idFun$TF$T$N$Any(p$arg: Ref) returns (ret$0: Ref)
+method f$idFun$TF$N$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()))
@@ -43,7 +43,7 @@ method f$checkMemberAccess$TF$() returns (ret$0: 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$T$N$Any(anon$0)
+  anon$7 := f$idFun$TF$N$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)
@@ -80,14 +80,14 @@ method f$checkMemberAccess$TF$() returns (ret$0: Ref)
   label lbl$ret$0
 }
 
-method f$idFun$TF$T$N$Any(p$arg: Ref) returns (ret: Ref)
+method f$idFun$TF$N$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$T$N$Any(p$wrapped: Ref) returns (ret: Ref)
+method con$c$Box$N$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)
@@ -120,7 +120,7 @@ method f$checkGenericMemberAccess$TF$T$c$Box(p$box: Ref)
   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$T$N$Any(anon$0)
+  anon$4 := f$idFun$TF$N$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)
@@ -133,7 +133,7 @@ method f$checkGenericMemberAccess$TF$T$c$Box(p$box: Ref)
   label lbl$ret$1
   unfold acc(p$c$Box$shared(p$box), wildcard)
   anon$8 := p$box.bf$wrapped
-  anon$7 := con$c$Box$T$N$Any(anon$8)
+  anon$7 := con$c$Box$N$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())
@@ -157,7 +157,7 @@ method f$checkGenericMemberAccess$TF$T$c$Box(p$box: Ref)
   label lbl$ret$0
 }
 
-method f$idFun$TF$T$N$Any(p$arg: Ref) returns (ret: Ref)
+method f$idFun$TF$N$Any(p$arg: Ref) returns (ret: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$nullable(df$rt$anyType()))
 
 
@@ -253,14 +253,14 @@ method f$accessManyMembers$TF$T$c$ManyMembers(p$m: Ref)
   anon$1 := anon$0
   unfold acc(p$c$ManyMembers$shared(anon$1), wildcard)
   anon$9 := anon$1.bf$i
-  anon$8 := f$idFun$TF$T$N$Any(anon$9)
+  anon$8 := f$idFun$TF$N$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$T$N$Any(anon$12)
+  anon$11 := f$idFun$TF$N$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)
@@ -278,20 +278,20 @@ method f$accessManyMembers$TF$T$c$ManyMembers(p$m: Ref)
   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$T$N$Any(anon$2)
+  anon$16 := f$idFun$TF$N$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$T$N$Any(anon$19)
+  anon$18 := f$idFun$TF$N$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$T$N$Any(anon$22)
+  anon$21 := f$idFun$TF$N$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)
@@ -311,7 +311,7 @@ method f$accessManyMembers$TF$T$c$ManyMembers(p$m: Ref)
   inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
 
-method f$idFun$TF$T$N$Any(p$arg: Ref) returns (ret: Ref)
+method f$idFun$TF$N$Any(p$arg: Ref) returns (ret: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$nullable(df$rt$anyType()))
 
 

plugins/formal-verification/testData/diagnostics/no_contracts/classes/predicates_access.fir.diag.txt

@@ -162,7 +162,7 @@ predicate p$c$A$unique(this$dispatch: Ref) {
   df$rt$isSubtype(df$rt$typeOf(this$dispatch.bf$a), df$rt$intType())
 }
 
-method f$accessNullable$TF$T$N$c$A(p$x: Ref) returns (ret$0: Ref)
+method f$accessNullable$TF$N$c$A(p$x: Ref) returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   var l0$n: Ref

plugins/formal-verification/testData/diagnostics/no_contracts/classes/primary_constructors.fir.diag.txt

@@ -25,7 +25,7 @@ method f$createPrimitiveFields$TF$() returns (ret$0: Ref)
 /primary_constructors.kt:(178,193): info: Generated Viper text for createRecursive:
 field bf$a: Ref
 
-method con$c$Recursive$T$N$c$Recursive(p$a: Ref) returns (ret: Ref)
+method con$c$Recursive$N$c$Recursive(p$a: Ref) returns (ret: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$T$c$Recursive())
   ensures acc(p$c$Recursive$shared(ret), wildcard)
   ensures acc(p$c$Recursive$unique(ret), write)
@@ -37,7 +37,7 @@ method f$createRecursive$TF$() returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$T$c$Recursive())
   ensures acc(p$c$Recursive$shared(ret$0), wildcard)
 {
-  ret$0 := con$c$Recursive$T$N$c$Recursive(df$rt$nullValue())
+  ret$0 := con$c$Recursive$N$c$Recursive(df$rt$nullValue())
   goto lbl$ret$0
   label lbl$ret$0
 }

plugins/formal-verification/testData/diagnostics/no_contracts/classes/subtyping.fir.diag.txt

@@ -1,5 +1,5 @@
 /subtyping.kt:(80,89): info: Generated Viper text for smartCast:
-method f$smartCast$TF$T$N$Int(p$x: Ref) returns (ret$0: Ref)
+method f$smartCast$TF$N$Int(p$x: Ref) returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$intType())
 {
   inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$nullable(df$rt$intType()))
@@ -38,10 +38,10 @@ method f$functionParameterSubtyping$TF$() returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   var anon$0: Ref
-  anon$0 := f$nullableParameter$TF$T$N$Boolean(df$rt$boolToRef(false))
+  anon$0 := f$nullableParameter$TF$N$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$T$N$Boolean(p$b: Ref) returns (ret: Ref)
+method f$nullableParameter$TF$N$Boolean(p$b: Ref) returns (ret: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$unitType())

plugins/formal-verification/testData/diagnostics/no_contracts/classes/unique_predicates.fir.diag.txt

@@ -67,7 +67,7 @@ predicate p$c$T$unique(this$dispatch: Ref) {
   true
 }
 
-method f$nullable_unique_arg$TF$T$N$c$T(p$t: Ref) returns (ret$0: Ref)
+method f$nullable_unique_arg$TF$N$c$T(p$t: Ref) returns (ret$0: Ref)
   requires p$t != df$rt$nullValue() ==> acc(p$c$T$unique(p$t), write)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {

plugins/formal-verification/testData/diagnostics/no_contracts/function_overloading.fir.diag.txt

@@ -72,7 +72,7 @@ method f$differInNullability$TF$T$Int(p$i: Ref) returns (ret$0: Ref)
 }
 
 /function_overloading.kt:(256,275): info: Generated Viper text for differInNullability:
-method f$differInNullability$TF$T$N$Int(p$i: Ref) returns (ret$0: Ref)
+method f$differInNullability$TF$N$Int(p$i: 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$i), df$rt$nullable(df$rt$intType()))

plugins/formal-verification/testData/diagnostics/no_contracts/operators/as_operator.fir.diag.txt

@@ -13,7 +13,7 @@ method f$testAs$TF$T$c$Foo(p$foo: Ref) returns (ret$0: Ref)
 }
 
 /as_operator.kt:(97,111): info: Generated Viper text for testNullableAs:
-method f$testNullableAs$TF$T$N$c$Foo(p$foo: Ref) returns (ret$0: Ref)
+method f$testNullableAs$TF$N$c$Foo(p$foo: Ref) returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$nullable(df$rt$T$c$Bar()))
   ensures ret$0 != df$rt$nullValue() ==>
     acc(p$c$Bar$shared(ret$0), wildcard)
@@ -49,7 +49,7 @@ method f$testSafeAs$TF$T$c$Foo(p$foo: Ref) returns (ret$0: Ref)
 }
 
 /as_operator.kt:(194,212): info: Generated Viper text for testNullableSafeAs:
-method f$testNullableSafeAs$TF$T$N$c$Foo(p$foo: Ref) returns (ret$0: Ref)
+method f$testNullableSafeAs$TF$N$c$Foo(p$foo: Ref) returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$nullable(df$rt$T$c$Bar()))
   ensures ret$0 != df$rt$nullValue() ==>
     acc(p$c$Bar$shared(ret$0), wildcard)