diff --git a/VSharp.CSharpUtils/Tests/Conditional.cs b/VSharp.CSharpUtils/Tests/Conditional.cs
index 0543a71ab..fd19588c4 100644
--- a/VSharp.CSharpUtils/Tests/Conditional.cs
+++ b/VSharp.CSharpUtils/Tests/Conditional.cs
@@ -139,5 +139,17 @@ public static int ExceptionInCondition3(NewBool nb)
                 return 56;
             }
         }
+
+        public static int DeclareAfterReturn(bool flag, bool f, int x)
+        {
+            if (f)
+            {
+                if (flag)
+                    return 42;
+                int y = x + x;
+                return x + x + y;
+            }
+            return x;
+        }
     }
 }
diff --git a/VSharp.SILI.Core/API.fs b/VSharp.SILI.Core/API.fs
index 8ce086b9a..fb40cc733 100644
--- a/VSharp.SILI.Core/API.fs
+++ b/VSharp.SILI.Core/API.fs
@@ -26,7 +26,8 @@ module API =
     let Explore id k = Explorer.explore id k
 
     let Call funcId state body k = Explorer.call m.Value funcId state body k
-    let InvokeAfter consumeContinue (result, state) statement k = ControlFlow.invokeAfter consumeContinue (result, state) statement k
+    let ComposeStatements rs statements isContinueConsumer reduceStatement k =
+        ControlFlow.composeStatements statements isContinueConsumer reduceStatement (fun state -> Memory.newScope m.Value state []) rs k
 
     let BranchStatements state condition thenBranch elseBranch k =
          Common.statedConditionalExecution state condition thenBranch elseBranch ControlFlow.mergeResults ControlFlow.merge2Results ControlFlow.throwOrIgnore k
diff --git a/VSharp.SILI.Core/API.fsi b/VSharp.SILI.Core/API.fsi
index 49272c08f..c652c15f9 100644
--- a/VSharp.SILI.Core/API.fsi
+++ b/VSharp.SILI.Core/API.fsi
@@ -15,7 +15,7 @@ module API =
     val Explore : IFunctionIdentifier -> (statementResult * state -> 'a) -> 'a
 
     val Call : IFunctionIdentifier -> state -> (state -> (statementResult * state -> 'a) -> 'a) -> (statementResult * state -> 'a) -> 'a
-    val InvokeAfter : bool -> (statementResult * state) -> (state -> (statementResult * state -> 'a) -> 'a) -> (statementResult * state -> 'a) -> 'a
+    val ComposeStatements : (statementResult * state) -> seq<'a> -> ('a -> bool) -> (state -> 'a -> (statementResult * state -> 'b) -> 'b) -> (statementResult * state -> 'b) -> 'b
 
     val BranchStatements : state -> (state -> (term * state -> 'a) -> 'b) -> (state -> (statementResult * state -> 'a) -> 'a) -> (state -> (statementResult * state -> 'a) -> 'a) -> (statementResult * state -> 'a) -> 'b
     val BranchExpressions : state -> (state -> (term * state -> 'a) -> 'b) -> (state -> (term * state -> 'a) -> 'a) -> (state -> (term * state -> 'a) -> 'a) -> (term * state -> 'a) -> 'b
diff --git a/VSharp.SILI.Core/ControlFlow.fs b/VSharp.SILI.Core/ControlFlow.fs
index 19cf98c90..edfdf6e59 100644
--- a/VSharp.SILI.Core/ControlFlow.fs
+++ b/VSharp.SILI.Core/ControlFlow.fs
@@ -111,14 +111,14 @@ module internal ControlFlow =
             match oldRes.result with
             | NoResult -> newRes
             | _ -> oldRes
-        match oldRes.result, newRes.result with
-        | NoResult, _ ->
+        match oldRes.result with
+        | NoResult ->
             newRes, newState
-        | Break, _
-        | Continue, _
-        | Throw _, _
-        | Return _, _ -> oldRes, oldState
-        | Guarded gvs, _ ->
+        | Break
+        | Continue
+        | Throw _
+        | Return _ -> oldRes, oldState
+        | Guarded gvs ->
             let conservativeGuard = List.fold (fun acc (g, v) -> if calculationDone v then acc ||| g else acc) False gvs
             let result =
                 match newRes.result with
@@ -132,18 +132,6 @@ module internal ControlFlow =
             let commonMetadata = Metadata.combine oldRes.metadata newRes.metadata
             Guarded commonMetadata result, Merging.merge2States conservativeGuard !!conservativeGuard oldState newState
 
-    let invokeAfter consumeContinue (result, state) statement k =
-        let pathCondition = currentCalculationPathCondition consumeContinue result
-        match pathCondition with
-        | Terms.True -> statement state (fun (newRes, newState) -> k (composeSequentially result newRes state newState))
-        | Terms.False -> k (result, state)
-        | _ ->
-            statement
-                (State.withPathCondition state pathCondition)
-                (fun (newRes, newState) ->
-                    let newState = State.popPathCondition newState
-                    k (composeSequentially result newRes state newState))
-
     let rec resultToTerm result =
         match result.result with
         | Return term -> Metadata.addMisc term (ReturnMarker()); { term = term.term; metadata = result.metadata }
@@ -173,6 +161,33 @@ module internal ControlFlow =
     let mergeResults grs =
         Merging.guardedMap resultToTerm grs |> throwOrReturn
 
+    let private invokeAfter consumeContinue (result, state) statement defaultCompose composeWithNewFrame k =
+        let pathCondition = currentCalculationPathCondition consumeContinue result
+        let compose newRS k =
+            if pathCondition = currentCalculationPathCondition consumeContinue (fst newRS)
+            then defaultCompose newRS k
+            else composeWithNewFrame newRS k
+        match pathCondition with //TODO: use statedConditionalExecution
+               | Terms.True -> statement state (fun newRS -> compose newRS k)
+               | Terms.False -> k (result, state)
+               | _ ->
+                   statement
+                       (State.withPathCondition state pathCondition)
+                       (fun (newRes, newState) -> compose (newRes, State.popPathCondition newState) k)
+
+
+    let composeStatements statements isContinueConsumer statementMapper newScope (result, state) k =
+        let rec composeStatementsH statements isContinueConsumer statementMapper newScope rs localk =
+            match statements with
+            | Seq.Empty -> k rs
+            | Seq.Cons(statement, tail) ->
+                let cmpseTailIfNeed newRS modSt ifLastk k = if Seq.isEmpty tail then ifLastk newRS else composeStatementsH tail isContinueConsumer statementMapper newScope (mapsnd modSt newRS) k
+                invokeAfter (isContinueConsumer statement) rs (fun state -> statementMapper state statement)
+                    (fun (newR, newS) k -> cmpseTailIfNeed (newR, newS) id k (fun (tailRes, tailState) -> k <| composeSequentially newR tailRes newS tailState))
+                    (fun (newR, newS) k -> cmpseTailIfNeed (newR, newS) newScope k (fun (tailRes, tailState) -> k <| composeSequentially newR tailRes newS (State.popStack tailState)))
+                    localk
+        composeStatementsH statements isContinueConsumer statementMapper newScope (result, state) (fun (newRes, newState) -> k <| composeSequentially result newRes state newState)
+
     let unguardResults gvs =
         let unguard gres =
             match gres with
diff --git a/VSharp.SILI/Interpreter.fs b/VSharp.SILI/Interpreter.fs
index dd4030860..383a40b7b 100644
--- a/VSharp.SILI/Interpreter.fs
+++ b/VSharp.SILI/Interpreter.fs
@@ -408,17 +408,11 @@ module internal Interpreter =
 // ------------------------------- Linear control flow-------------------------------
 
     and reduceSequentially state statements k =
-        Cps.Seq.foldlk
-            (InvokeAfter false)
-            (NoResult(), Memory.NewScope state [])
-            statements
-            (fun (res, state) -> k (res, Memory.PopStack state))
+        ComposeStatements (NoResult(), Memory.NewScope state []) statements (always false) (fun state stmt -> stmt state) (fun (res, state) -> k (res, Memory.PopStack state))
 
     and reduceBlockStatement state (ast : IBlockStatement) k =
-        let compose rs statement k =
-            InvokeAfter (Transformations.isContinueConsumer statement) rs (fun state -> reduceStatement state statement) k
         let k = Enter ast state k
-        Cps.Seq.foldlk compose (NoResult(), Memory.NewScope state []) ast.Statements (fun (res, state) -> k (res, Memory.PopStack state))
+        ComposeStatements (NoResult(), Memory.NewScope state []) ast.Statements Transformations.isContinueConsumer reduceStatement (fun (res, state) -> k (res, Memory.PopStack state))
 
     and reduceCommentStatement state (ast : ICommentStatement) k =
         k (NoComputation, state)
@@ -1066,24 +1060,21 @@ module internal Interpreter =
                 let state = Memory.NewScope state [((tempVar, tempVar), Specified freshValue, TypeOf freshValue)]
                 (Memory.ReferenceLocalVariable state (tempVar, tempVar) false, state)
         initializeStaticMembersIfNeed caller state qualifiedTypeName (fun (result, state) ->
-        let finish r =
-            InvokeAfter false r
-                (fun state k ->
-                    if isReferenceType || returnRef
-                    then k (Return reference, state)
-                    else
-                        let term, state = Memory.Dereference state reference
-                        k (Return term, Memory.PopStack state))
-                (fun (result, state) -> k (ControlFlow.ResultToTerm result, state))
         let invokeInitializers result state (result', state') =
             let r = ControlFlow.ComposeSequentially result result' state state'
-            InvokeAfter false r (fun state k ->
+            let reduceInitializers state k =
                 if objectInitializerList <> null then
                     reduceMemberInitializerList reference state objectInitializerList k
                 elif collectionInitializerList <> null then
                     reduceCollectionInitializerList constructedType reference state collectionInitializerList k
                 else k (NoComputation, state)
-            ) finish
+            let finish state k =
+                if isReferenceType || returnRef
+                then k (Return reference, state)
+                else
+                    let term, state = Memory.Dereference state reference
+                    k (Return term, Memory.PopStack state)
+            ComposeStatements r (seq[reduceInitializers; finish]) (always false) (fun state stmt -> stmt state) (fun (result, state) -> k (ControlFlow.ResultToTerm result, state))
         if constructorSpecification = null
             then invokeInitializers result state (NoResult(), state)
             else
diff --git a/VSharp.Test/Tests/VSharp.CSharpUtils/Unix.gold b/VSharp.Test/Tests/VSharp.CSharpUtils/Unix.gold
index c7c00d6fb..7a63b669c 100644
--- a/VSharp.Test/Tests/VSharp.CSharpUtils/Unix.gold
+++ b/VSharp.Test/Tests/VSharp.CSharpUtils/Unix.gold
@@ -3240,6 +3240,15 @@ System.Runtime.Serialization.SafeSerializationManager ==> STRUCT System.Runtime.
 System.SystemException ==> STRUCT System.SystemException[]
 VSharp.CSharpUtils.Tests.Conditional+NewBool ==> STRUCT VSharp.CSharpUtils.Tests.Conditional+NewBool[]
 VSharp.CSharpUtils.Tests.Conditional ==> STRUCT VSharp.CSharpUtils.Tests.Conditional[]
+METHOD: System.Int32 VSharp.CSharpUtils.Tests.Conditional.DeclareAfterReturn(System.Boolean, System.Boolean, System.Int32)
+RESULT: UNION[
+	| !f ~> x
+	| !flag & f ~> x + x + x + x
+	| f & flag ~> 42]
+HEAP:
+{ heap = <empty>, statics = s0 } where
+---------- s0 = ----------
+VSharp.CSharpUtils.Tests.Conditional ==> STRUCT VSharp.CSharpUtils.Tests.Conditional[]
 METHOD: System.Int32 VSharp.CSharpUtils.Tests.Fibonacci.Fib2()
 RESULT: 2
 HEAP:
@@ -3901,9 +3910,9 @@ System.SystemException ==> STRUCT System.SystemException[]
 VSharp.CSharpUtils.Tests.Lists ==> STRUCT VSharp.CSharpUtils.Tests.Lists[]
 METHOD: System.Array VSharp.CSharpUtils.Tests.Lists.RetSystemArray2(System.Array)
 RESULT: UNION[
-	| !(0 == arr) & (!(0 == arr) & !(1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & !(1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[,]) & (ArrayTypeVariable1 <: int32[])) & (!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (ArrayTypeVariable1 <: int32[,,]) | (!(0 == arr) & !(1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & !(1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[,]) & (ArrayTypeVariable1 <: int32[])) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(ArrayTypeVariable1 <: int32[,,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) ~> <ERROR: (HeapRef 1)>
-	| !(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[]) | 1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[,,]) & (ArrayTypeVariable1 <: int32[,]) | !(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[]) | 1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(ArrayTypeVariable1 <: int32[,,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) & (ArrayTypeVariable1 <: int32[,]) ~> <ERROR: (HeapRef 6)>
+	| !(0 == arr) & !(1 < arr.0_Length) & (!(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (ArrayTypeVariable1 <: int32[,,]) & (ArrayTypeVariable1 <: int32[,]) | !(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(ArrayTypeVariable1 <: int32[,,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) & (ArrayTypeVariable1 <: int32[,])) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & !(1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(ArrayTypeVariable1 <: int32[,,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & !(1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[,,]) & (ArrayTypeVariable1 <: int32[]) ~> <ERROR: (HeapRef 1)>
 	| !(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(ArrayTypeVariable1 <: int32[]) | 1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[,,]) ~> <ERROR: (HeapRef 9)>
+	| (!(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (ArrayTypeVariable1 <: int32[,,]) & (ArrayTypeVariable1 <: int32[,]) | !(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(ArrayTypeVariable1 <: int32[,,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) & (ArrayTypeVariable1 <: int32[,])) & (!(ArrayTypeVariable1 <: int32[]) | 0 == arr | 1 < arr.0_Length) ~> <ERROR: (HeapRef 6)>
 	| (!(ArrayTypeVariable1 <: int32[]) | 0 == arr | 1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(ArrayTypeVariable1 <: int32[,,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) ~> (HeapRef arr)]
 HEAP:
 { heap = h0, statics = s1 } where
@@ -3986,11 +3995,11 @@ HEAP:
 	| System.Exception.native_trace_ips ~> null]
 arr ==> TypeVariable1{System.Object}: [|
 	1, 1, 1: UNION[
-		| !(0 == arr) & (!(1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[]) | !(ArrayTypeVariable1 <: int32[,]) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[,,]) & 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length ~> 42];
+		| !(0 == arr) & (!(ArrayTypeVariable1 <: int32[,]) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[,,]) & 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length ~> 42];
 	1, 1: UNION[
-		| !(0 == arr) & (!(0 == arr) & !(1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & !(1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[,]) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[]) | 1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[,])) & (ArrayTypeVariable1 <: int32[,]) & 1 < arr.0_Length & 1 < arr.1_Length | !(0 == arr) & (!(1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[]) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[,]) & 1 < arr.0_Length & 1 < arr.1_Length ~> 7];
+		| !(0 == arr) & (ArrayTypeVariable1 <: int32[,]) & 1 < arr.0_Length & 1 < arr.1_Length ~> 7];
 	1: UNION[
-		| !(0 == arr) & (!(0 == arr) & !(1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & !(1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[,]) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[]) | 1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[,])) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length | (!(0 == arr) & !(ArrayTypeVariable1 <: int32[,,]) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length | !(0 == arr) & (!(0 == arr) & (!(1 < arr.1_Length) | !(1 < arr.2_Length)) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length | !(0 == arr) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) & (ArrayTypeVariable1 <: int32[,,])) & (!(1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[]) | !(ArrayTypeVariable1 <: int32[,]) | 0 == arr | 1 < arr.0_Length & 1 < arr.1_Length) & (!(ArrayTypeVariable1 <: int32[,]) | !(ArrayTypeVariable1 <: int32[]) | 0 == arr | 1 < arr.0_Length) & (!(ArrayTypeVariable1 <: int32[]) | (!(0 == arr) & (ArrayTypeVariable1 <: int32[,]) | 1 < arr.0_Length & 1 < arr.1_Length) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) | 0 == arr | 1 < arr.0_Length) ~> 5];
+		| (!(0 == arr) & !(1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[,]) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length | (!(0 == arr) & !(ArrayTypeVariable1 <: int32[,,]) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length | !(0 == arr) & (!(0 == arr) & (!(1 < arr.1_Length) | !(1 < arr.2_Length)) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length | !(0 == arr) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) & (ArrayTypeVariable1 <: int32[,,])) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr | 1 < arr.0_Length & 1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[]) | 0 == arr | 1 < arr.0_Length) ~> 5];
 	 ...  ... |]
 ---------- s1 = ----------
 System.Environment ==> STRUCT System.Environment[
diff --git a/VSharp.Test/Tests/VSharp.CSharpUtils/Win32NT.gold b/VSharp.Test/Tests/VSharp.CSharpUtils/Win32NT.gold
index 1baff0c2a..2731e9c0a 100644
--- a/VSharp.Test/Tests/VSharp.CSharpUtils/Win32NT.gold
+++ b/VSharp.Test/Tests/VSharp.CSharpUtils/Win32NT.gold
@@ -3860,6 +3860,15 @@ HEAP:
 { heap = <empty>, statics = s0 } where
 ---------- s0 = ----------
 VSharp.CSharpUtils.Tests.Fibonacci ==> STRUCT VSharp.CSharpUtils.Tests.Fibonacci[]
+METHOD: System.Int32 VSharp.CSharpUtils.Tests.Conditional.DeclareAfterReturn(System.Boolean, System.Boolean, System.Int32)
+RESULT: UNION[
+	| !f ~> x
+	| !flag & f ~> x + x + x + x
+	| f & flag ~> 42]
+HEAP:
+{ heap = <empty>, statics = s0 } where
+---------- s0 = ----------
+VSharp.CSharpUtils.Tests.Conditional ==> STRUCT VSharp.CSharpUtils.Tests.Conditional[]
 METHOD: System.Int32 VSharp.CSharpUtils.Tests.Fibonacci.FibUnbound(System.Int32)
 RESULT: UNION[
 	| !(-1 + n < 2) & !(n < 2) ~> 42 + VSharp.CSharpUtils.Tests.Fibonacci._a + VSharp.CSharpUtils.Tests.Fibonacci._b + VSharp.CSharpUtils.Tests.Fibonacci._a + VSharp.CSharpUtils.Tests.Fibonacci._b + VSharp.CSharpUtils.Tests.Fibonacci._b
@@ -4672,9 +4681,9 @@ System.ValueType ==> STRUCT System.ValueType[]
 VSharp.CSharpUtils.Tests.Lists ==> STRUCT VSharp.CSharpUtils.Tests.Lists[]
 METHOD: System.Array VSharp.CSharpUtils.Tests.Lists.RetSystemArray2(System.Array)
 RESULT: UNION[
-	| !(0 == arr) & (!(0 == arr) & !(1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & !(1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[,]) & (ArrayTypeVariable1 <: int32[])) & (!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (ArrayTypeVariable1 <: int32[,,]) | (!(0 == arr) & !(1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & !(1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[,]) & (ArrayTypeVariable1 <: int32[])) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(ArrayTypeVariable1 <: int32[,,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) ~> <ERROR: (HeapRef 1)>
-	| !(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[]) | 1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[,,]) & (ArrayTypeVariable1 <: int32[,]) | !(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[]) | 1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(ArrayTypeVariable1 <: int32[,,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) & (ArrayTypeVariable1 <: int32[,]) ~> <ERROR: (HeapRef 6)>
+	| !(0 == arr) & !(1 < arr.0_Length) & (!(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (ArrayTypeVariable1 <: int32[,,]) & (ArrayTypeVariable1 <: int32[,]) | !(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(ArrayTypeVariable1 <: int32[,,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) & (ArrayTypeVariable1 <: int32[,])) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & !(1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(ArrayTypeVariable1 <: int32[,,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & !(1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[,,]) & (ArrayTypeVariable1 <: int32[]) ~> <ERROR: (HeapRef 1)>
 	| !(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(ArrayTypeVariable1 <: int32[]) | 1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[,,]) ~> <ERROR: (HeapRef 9)>
+	| (!(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (ArrayTypeVariable1 <: int32[,,]) & (ArrayTypeVariable1 <: int32[,]) | !(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(ArrayTypeVariable1 <: int32[,,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) & (ArrayTypeVariable1 <: int32[,])) & (!(ArrayTypeVariable1 <: int32[]) | 0 == arr | 1 < arr.0_Length) ~> <ERROR: (HeapRef 6)>
 	| (!(ArrayTypeVariable1 <: int32[]) | 0 == arr | 1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length) | !(1 < arr.2_Length)) & (!(ArrayTypeVariable1 <: int32[,,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) ~> (HeapRef arr)]
 HEAP:
 { heap = h0, statics = s1 } where
@@ -4775,11 +4784,11 @@ HEAP:
 		| System.IntPtr.m_value ~> 0]]
 arr ==> TypeVariable1{System.Object}: [|
 	1, 1, 1: UNION[
-		| !(0 == arr) & (!(1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[]) | !(ArrayTypeVariable1 <: int32[,]) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[,,]) & 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length ~> 42];
+		| !(0 == arr) & (!(ArrayTypeVariable1 <: int32[,]) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[,,]) & 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length ~> 42];
 	1, 1: UNION[
-		| !(0 == arr) & (!(0 == arr) & !(1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & !(1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[,]) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[]) | 1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[,])) & (ArrayTypeVariable1 <: int32[,]) & 1 < arr.0_Length & 1 < arr.1_Length | !(0 == arr) & (!(1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[]) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[,]) & 1 < arr.0_Length & 1 < arr.1_Length ~> 7];
+		| !(0 == arr) & (ArrayTypeVariable1 <: int32[,]) & 1 < arr.0_Length & 1 < arr.1_Length ~> 7];
 	1: UNION[
-		| !(0 == arr) & (!(0 == arr) & !(1 < arr.0_Length) & ((!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr) | 1 < arr.0_Length & 1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & !(1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[,]) & (ArrayTypeVariable1 <: int32[]) | !(0 == arr) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[]) | 1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[,])) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length | (!(0 == arr) & !(ArrayTypeVariable1 <: int32[,,]) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length | !(0 == arr) & (!(0 == arr) & (!(1 < arr.1_Length) | !(1 < arr.2_Length)) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length | !(0 == arr) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) & (ArrayTypeVariable1 <: int32[,,])) & (!(1 < arr.0_Length) & (ArrayTypeVariable1 <: int32[]) | !(ArrayTypeVariable1 <: int32[,]) | 0 == arr | 1 < arr.0_Length & 1 < arr.1_Length) & (!(ArrayTypeVariable1 <: int32[,]) | !(ArrayTypeVariable1 <: int32[]) | 0 == arr | 1 < arr.0_Length) & (!(ArrayTypeVariable1 <: int32[]) | (!(0 == arr) & (ArrayTypeVariable1 <: int32[,]) | 1 < arr.0_Length & 1 < arr.1_Length) & (!(1 < arr.0_Length) | !(1 < arr.1_Length)) | 0 == arr | 1 < arr.0_Length) ~> 5];
+		| (!(0 == arr) & !(1 < arr.1_Length) & (ArrayTypeVariable1 <: int32[,]) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length | (!(0 == arr) & !(ArrayTypeVariable1 <: int32[,,]) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length | !(0 == arr) & (!(0 == arr) & (!(1 < arr.1_Length) | !(1 < arr.2_Length)) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length | !(0 == arr) & (ArrayTypeVariable1 <: int32[]) & 1 < arr.0_Length & 1 < arr.1_Length & 1 < arr.2_Length) & (ArrayTypeVariable1 <: int32[,,])) & (!(ArrayTypeVariable1 <: int32[,]) | 0 == arr | 1 < arr.0_Length & 1 < arr.1_Length)) & (!(ArrayTypeVariable1 <: int32[]) | 0 == arr | 1 < arr.0_Length) ~> 5];
 	 ...  ... |]
 ---------- s1 = ----------
 System.Environment ==> STRUCT System.Environment[