Create new state internal id on copy.

PySymGym · Dec 22, 2023 · a5efef2 · a5efef2
1 parent e4a3767
commit a5efef2
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 2 deletions.
diff --git a/VSharp.Explorer/Explorer.fs b/VSharp.Explorer/Explorer.fs
@@ -305,6 +305,11 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM
                 sIsStopped <- true
                 goodStates @ iieStates @ errors
         Application.moveState loc s (Seq.cast<_> newStates)
+        for newState in newStates do
+            let historyCopy = System.Collections.Generic.Dictionary<_,_>()
+            for kvp in s._history do historyCopy.Add(kvp.Key, kvp.Value)
+            newState._history <- historyCopy
+        s.children <- s.children @ newStates
         statistics.TrackFork s newStates
         searcher.UpdateStates s newStates
         if sIsStopped then

diff --git a/VSharp.SILI/CILState.fs b/VSharp.SILI/CILState.fs
@@ -104,7 +104,7 @@ module CilState =
             /// <summary>
             /// Deterministic state id.
             /// </summary>
-            internalId : uint<VSharp.ML.GameServer.Messages.stateId>
+            mutable internalId : uint<VSharp.ML.GameServer.Messages.stateId>
             mutable visitedAgainVertices: uint
             mutable visitedNotCoveredVerticesInZone: uint
             mutable visitedNotCoveredVerticesOutOfZone: uint
@@ -447,7 +447,10 @@ module CilState =
             let clone = { x with state = x.state }
             let mkCilState state' =
                 if LanguagePrimitives.PhysicalEquality state' x.state then x
-                else clone.Copy(state')
+                else
+                    let s = clone.Copy(state')
+                    s.internalId <- getNextStateId()
+                    s
             StatedConditionalExecution x.state conditionInvocation
                 (fun state k -> thenBranch (mkCilState state) k)
                 (fun state k -> elseBranch (mkCilState state) k)