From 0fe20ba75e36a069844be8a095824739ad4d7124 Mon Sep 17 00:00:00 2001 From: Anya497 Date: Wed, 26 Mar 2025 18:11:06 +0300 Subject: [PATCH] Add path condition root to GameState. --- VSharp.IL/Serializer.fs | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/VSharp.IL/Serializer.fs b/VSharp.IL/Serializer.fs index f42e9d46f..182dd899a 100644 --- a/VSharp.IL/Serializer.fs +++ b/VSharp.IL/Serializer.fs @@ -488,15 +488,20 @@ let collectGameState (basicBlocks: ResizeArray) filterStates = for term in pathCondition do pathConditionDelta.AddRange(collectPathCondition term) - State( - s.Id, - (uint <| s.CodeLocation.offset - currentBasicBlock.StartOffset + 1) - * 1u, + let pathConditionRoot = PathConditionVertex( id = getFirstFreePathConditionVertexId (), pathConditionVertexType = pathConditionVertexType.PathConditionRoot, children = [| for p in pathCondition -> pathConditionVertices.[p].Id |] - ), + ) + + pathConditionDelta.Add pathConditionRoot + + State( + s.Id, + (uint <| s.CodeLocation.offset - currentBasicBlock.StartOffset + 1) + * 1u, + pathConditionRoot, s.VisitedAgainVertices, s.VisitedNotCoveredVerticesInZone, s.VisitedNotCoveredVerticesOutOfZone,