[style] fixed style

VSharp.API/VSharpOptions.cs

@@ -125,7 +125,6 @@ public readonly record struct VSharpOptions
     /// <param name="releaseBranches">If true and timeout is specified, a part of allotted time in the end is given to execute remaining states without branching.</param>
     /// <param name="randomSeed">Fixed seed for random operations. Used if greater than or equal to zero.</param>
     /// <param name="stepsLimit">Number of symbolic machine steps to stop execution after. Zero value means no limit.</param>
-
     public VSharpOptions(
         int timeout = DefaultTimeout,
         int solverTimeout = DefaultSolverTimeout,

VSharp.SILI/CILState.fs

@@ -235,7 +235,7 @@ module CilState =
             x.SetCurrentIp ip
 
         member x.ReplaceLastIp (ip : instructionPointer) =
-            let newIp = x.CurrentIp.ReplacePenultimateIp ip
+            let newIp = x.CurrentIp.ReplaceRecIp ip
             x.SetCurrentIp newIp
 
         member x.MarkExit (m : Method) =

VSharp.SILI/InstructionPointer.fs

@@ -37,22 +37,24 @@ type instructionPointer =
             SecondBypass(Some (ip.ChangeInnerIp newIp), ehcs, lastBlocks, loc, cl, ftp)
         | _ -> newIp
 
-    member internal x.ReplacePenultimateIp newIp =
-        let (|NonRecIp|_|) = function
-            | Instruction _ -> Some ()
-            | Exit _ -> Some ()
-            | SearchingForHandler _ -> Some ()
-            | SecondBypass(None, _, _, _, _, _) -> Some()
-            | _ -> None
+    member private x.IsNonRecIp with get() =
         match x with
-        | InFilterHandler(NonRecIp, _, _, _, _, _)
-        | Leave(NonRecIp, _, _, _)
-        | SecondBypass(Some NonRecIp, _, _, _, _, _) -> newIp
+        | Instruction _
+        | Exit _
+        | SearchingForHandler _
+        | SecondBypass(None, _, _, _, _, _) -> true
+        | _ -> false
+
+    member internal x.ReplaceRecIp newIp =
+        match x with
+        | InFilterHandler(ip, _, _, _, _, _)
+        | Leave(ip, _, _, _)
+        | SecondBypass(Some ip, _, _, _, _, _) when ip.IsNonRecIp -> newIp
         | InFilterHandler(ip, offset, e, f, lc, l) ->
-            InFilterHandler(ip.ReplacePenultimateIp newIp, offset, e, f, lc, l)
-        | Leave(ip, e, i, m) -> Leave(ip.ReplacePenultimateIp newIp, e, i, m)
+            InFilterHandler(ip.ReplaceRecIp newIp, offset, e, f, lc, l)
+        | Leave(ip, e, i, m) -> Leave(ip.ReplaceRecIp newIp, e, i, m)
         | SecondBypass(Some ip, ehcs, lastBlocks, lastLocation, locations, handlerLoc) ->
-            SecondBypass(Some (ip.ReplacePenultimateIp newIp), ehcs, lastBlocks, lastLocation, locations, handlerLoc)
+            SecondBypass(Some (ip.ReplaceRecIp newIp), ehcs, lastBlocks, lastLocation, locations, handlerLoc)
         | _ -> newIp
 
     member internal x.MoveInstruction (newOffset : offset) =
@@ -162,10 +164,6 @@ type level = pdict<codeLocation, uint32>
 
 module IpOperations =
 
-    let exit m = Exit m
-
-    let instruction m i = Instruction(i, m)
-
     let bypassShouldPopFrame bypassLocations locationToJump currentLoc =
         List.isEmpty bypassLocations |> not ||
         match locationToJump with
@@ -223,9 +221,3 @@ module Level =
     let levelToUnsignedInt (lvl : level) =
         // TODO: remove it when ``level'' subtraction would be generalized
         PersistentDict.fold (fun acc _ v -> max acc v) 0u lvl
-
-    let composeLevel (lvl1 : level) (lvl2 : level) =
-        let composeOne (lvl : level) k v =
-            let oldValue = PersistentDict.tryFind lvl k |> Option.defaultValue 0u
-            PersistentDict.add k (v + oldValue) lvl
-        PersistentDict.fold composeOne lvl1 lvl2

VSharp.SILI/Interpreter.fs

@@ -638,7 +638,7 @@ type ILInterpreter() as this =
 
     static member InitFunctionFrameCIL (cilState : cilState) (method : Method) this paramValues =
         Memory.InitFunctionFrame cilState.state method this (paramValues |> Option.bind (List.map Some >> Some))
-        cilState.PushToIp (instruction method 0<offsets>)
+        Instruction(0<offsets>, method) |> cilState.PushToIp
 
     static member CheckDisallowNullAttribute (method : Method) (argumentsOpt : term list option) (cilState : cilState) shouldReportError k =
         if not <| method.CheckAttributes then
@@ -1547,7 +1547,7 @@ type ILInterpreter() as this =
                 cilState.Push errorRef
                 cilState.NewExceptionRegister()
                 let handlerOffset = ehc.handlerOffset
-                let filterHandler = instruction method o
+                let filterHandler = Instruction(o, method)
                 let observed = List.ofSeq observed
                 nextIp <- Some (InFilterHandler(filterHandler, handlerOffset, ehcs, observed, locations, framesToPop))
             | _ -> () // Handler is non-suitable catch or finally

VSharp.Solver/Z3.fs

@@ -176,7 +176,7 @@ module internal Z3 =
                 keySet.Add(key) |> ignore
                 regionAccesses.Add(typ, keySet)
 
-        let regionAccessExists (m : Model) (typ : regionSort * path) (storeKey : Expr[]) =
+        let tryRemoveRegionAccess (m : Model) (typ : regionSort * path) (storeKey : Expr[]) =
             let keySet = encodingCache.regionAccesses[typ]
             let mutable toDelete = None
             for k in keySet do
@@ -1359,7 +1359,7 @@ module internal Z3 =
                         elif arr.IsStore then
                             assert(arr.Args.Length >= 3)
                             let key = arr.Args[1..arr.Args.Length - 2]
-                            let shouldStore = not containsAddress || regionAccessExists m typ key
+                            let shouldStore = not containsAddress || tryRemoveRegionAccess m typ key
                             parseArray arr.Args[0]
                             if shouldStore then
                                 let value = Array.last arr.Args |> x.Decode typeOfLocation