diff --git a/src/base/SMPFunctionSPARK.cpp b/src/base/SMPFunctionSPARK.cpp index 23c160c5550f66aa2333d68375e19fe0fe5e0865..9a7b8d1a55def3bbc4787b781a224d9d23ef9b90 100644 --- a/src/base/SMPFunctionSPARK.cpp +++ b/src/base/SMPFunctionSPARK.cpp @@ -2098,6 +2098,7 @@ int SMPFunction::FindConditionalFollowNode4(const int HeadBlockNum, bool &IfThen OddIfThenCase = false; IfThenElseCase = false; FollowBlockNum = SMP_BLOCKNUM_UNINIT; + this->SPARKCloningWorkList.clear(); // Reverse earlier decision to fix by cloning. } } } @@ -2200,7 +2201,6 @@ bool SMPFunction::SolveConditionalDomFrontierProblemViaCloning(const int HeadBlo SMP_msg("INFO: SPARK: CLONING 4: Cloning from %d to %d would solve DomFrontier non-convergence for HeadBlock %d ", NFTDomFrontierBlockNum, FTDomFrontierBlockNum, HeadBlockNum); this->DumpFuncNameAndAddr(); this->DumpDotCFG(); - this->ResetTCFGVisitedBlocks(); FollowBlockNum = FTDomFrontierBlockNum; CloningStructuresConditional = true; this->ResetTCFGVisitedBlocks();