diff --git a/include/base/SMPDataFlowAnalysis.h b/include/base/SMPDataFlowAnalysis.h
index d9a4f4f5363f1a9812211df7e9376902a0a5825a..d455c57150855bdb7657c93f489e9b65af24fb9b 100644
--- a/include/base/SMPDataFlowAnalysis.h
+++ b/include/base/SMPDataFlowAnalysis.h
@@ -93,7 +93,7 @@ class STARSBitSet;
 #define SMP_SSA_UNINIT  (-1)
 
 // Bit masks for extracting bits from a STARSBitSet unsigned char.
-extern const unsigned char STARSBitMasks[8];
+extern const uint8_t STARSBitMasks[8];
 
 // Map register number to a string for printing or annotations.
 extern const char *RegNames[];
@@ -1035,21 +1035,25 @@ public:
 	// Get methods
 	bool GetBit(std::size_t BitIndex) const;
 	std::size_t GetNumBits(void) const { return BitLimit; };
+	uint8_t GetByte(std::size_t ByteIndex) const;
 	// Set methods
 	void AllocateBits(std::size_t Size); // allocate Size bits, initialized to zero.
 	void SetBit(std::size_t BitIndex);
 	void ResetBit(std::size_t BitIndex);
+	void SetByte(const std::size_t ByteIndex, const uint8_t ByteValue);
 	void UnionSets(const STARSBitSet &BitSet2);
 	// Query methods
 	bool IsAnyBitSet(void) const; // Returns false if all bits are zero, true otherwise.
 	int FindHighestBitSet(void) const; // Return highest index set; -1 if no bits set.
 	int FindLowestBitSet(void) const; // Return lowest index set; -1 if no bits set.
-	size_t CountSetBits(void) const; // return count of set bits
+	std::size_t CountSetBits(void) const; // return count of set bits
+	// Print methods
+	void DumpBitsSet(void) const; // Debugging output of bits set
 
 private:
 	// Data members.
 	std::size_t BitLimit; // number of bits
-	std::vector<unsigned char> STARSBits;
+	std::vector<uint8_t> STARSBits;
 	// Methods
 }; // end class STARSBitSet
 
@@ -1138,7 +1142,7 @@ unsigned int CountBitsSet(unsigned int ArgPosBits);
 
 // Utility to get highest bit set in a byte.
 // Assumes that Byte is non-zero and has some bit set.
-unsigned int HighestBitSet(unsigned char Byte);
+unsigned int HighestBitSet(uint8_t Byte);
 
 // Utility to get lowest bit set in a byte.
 // Assumes that Byte is non-zero and has some bit set.
diff --git a/include/base/SMPFunction.h b/include/base/SMPFunction.h
index dbfaf3c4095d44227ff60828d9f2c71a4f07dd88..ea409be7e9c2ca4b323e1e9c44a13be461eba69a 100644
--- a/include/base/SMPFunction.h
+++ b/include/base/SMPFunction.h
@@ -786,6 +786,7 @@ private:
 	std::vector<int> LoopTestBlocksByLoopNum; // indexed by loop number; block number of header block for top-testing or tail block for bottom-testing, -1 for middle-testing
 	std::vector<int> LoopHeadBlockNumbers; // indexed by loop number; block number of header block
 	std::vector<std::set<int> > LoopFollowNodes; // indexed by loop number; block number of follow block
+	std::vector<std::map<int, STARSBitSet> > LoopFollowNodesReachabilitySets; // indexed by LoopNum, map exit target block num to bitset of block nums downward reachable from exit block num; SPARK-useful if multiple exit block targets
 	std::vector<bool> LoopHasMultipleExits; 
 	std::vector<bool> LoopWritesMemory; // static, indirect or indexed writes
 	std::vector<bool> LoopReadsMemory; // static, indirect or indexed reads
@@ -972,6 +973,8 @@ private:
 	void DetectLoopFollowBlock(const std::size_t LoopNumber); // Detect successor blocks not in loop; if not exactly one, not structured CFG.
 	void ClassifyLoop(std::size_t LoopNumber, int HeaderExitFollowNum, int TailExitFollowNum, SMPBasicBlock *CurrBlock, SMPBasicBlock *HeadBlock, bool HeaderBlockExitsLoop, bool TailBlockExitsLoop); // classify LoopNumber loop as top, middle, or bottom testing
 	bool DoesBlockExitLoop(std::size_t LoopNumber, SMPBasicBlock *LoopBlock, int &FollowBlockNum); // return true if block can exit the loop.
+	void ComputeLoopFollowNodesReachability(const std::size_t LoopNum); // populate entry in LoopFollowNodesReachabilitySets
+	void MarkReachableBlocks(const int BlockNum, STARSBitSet &ReachableSet); // Set bits of current BlockNum and its descendants in CFG
 	void DetectLoopInvariantDEFs(void); // Collect a set of loop-invariant DEFs with the inst IDs of the DEFs.
 	void DetectLoopInvariantDEFs2(void); // Collect a set of loop-invariant DEFs with the inst IDs of the DEFs.
 	bool IsUseLoopInvariantDEF(std::size_t LoopIndex, const STARSOpndTypePtr &UseOp, SMPInstr *UseInst); // Track UseOp to its DEF, see if loop-invariant for LoopIndex
diff --git a/src/base/SMPDataFlowAnalysis.cpp b/src/base/SMPDataFlowAnalysis.cpp
index f5e3ed84ad0491df54d6a3d9d00d5ff1b34666c7..446174e9ee19eedc2f60d1b02421476f261ca8a7 100644
--- a/src/base/SMPDataFlowAnalysis.cpp
+++ b/src/base/SMPDataFlowAnalysis.cpp
@@ -72,7 +72,7 @@ bool IsIntInList(const std::list<int> &IntList, int Item) {
 }
 
 // Bit masks for extracting bits from a STARSBitSet unsigned char.
-const unsigned char STARSBitMasks[8] = { 1, 2, 4, 8, 16, 32, 64, 128 };
+const uint8_t STARSBitMasks[8] = { 1, 2, 4, 8, 16, 32, 64, 128 };
 
 const char *RegNames[MAX_IDA_REG + 1] =
 	{ "EAX", "ECX", "EDX", "EBX", "ESP", "EBP", "ESI", "EDI",
@@ -3869,7 +3869,12 @@ bool STARSBitSet::GetBit(size_t BitIndex) const {
 	size_t ByteIndex = BitIndex / 8;
 	size_t BitNumber = BitIndex % 8;
 	assert(BitIndex <= this->BitLimit);
-	return (0 != (this->STARSBits.at(ByteIndex) & STARSBitMasks[BitNumber]));
+	return (0 != (this->STARSBits[ByteIndex] & STARSBitMasks[BitNumber]));
+}
+
+uint8_t STARSBitSet::GetByte(std::size_t ByteIndex) const {
+	assert(ByteIndex < this->STARSBits.size());
+	return this->STARSBits[ByteIndex];
 }
 
 // Set methods
@@ -3940,7 +3945,7 @@ int STARSBitSet::FindHighestBitSet(void) const {
 	else {
 		return -1;
 	}
-}
+} // end of STARSBitSet::FindHighestBitSet()
 
 // Return lowest index set; -1 if no bits set.
 int STARSBitSet::FindLowestBitSet(void) const {
@@ -3968,7 +3973,7 @@ size_t STARSBitSet::CountSetBits(void) const {
 	size_t ByteIndex, BitCount = 0, BitSetSize = this->STARSBits.size();
 	assert(0 < BitSetSize);
 	for (ByteIndex = 0; ByteIndex < BitSetSize; ++ByteIndex) {
-		unsigned char CurrByte = this->STARSBits[ByteIndex];
+		uint8_t CurrByte = this->STARSBits[ByteIndex];
 		if (0 != CurrByte) {
 			BitCount += CountBitsSet((unsigned int) CurrByte);
 		}
@@ -3976,14 +3981,37 @@ size_t STARSBitSet::CountSetBits(void) const {
 	return BitCount;
 } // end of STARSBitSet::CountSetBits()
 
+// Debugging output of bits set
+void STARSBitSet::DumpBitsSet(void) const {
+	size_t ByteIndex, BitCount = 0, BitSetSize = this->STARSBits.size();
+	assert(0 < BitSetSize);
+	for (ByteIndex = 0; ByteIndex < BitSetSize; ++ByteIndex) {
+		uint8_t CurrByte = this->STARSBits[ByteIndex];
+		if (0 != CurrByte) {
+			size_t CurrBitLimit = 8 + (8 * ByteIndex);
+			if (CurrBitLimit > this->GetNumBits())
+				CurrBitLimit = this->GetNumBits();
+			for (size_t BitIndex = 8 * ByteIndex; BitIndex < CurrBitLimit; ++BitIndex) {
+				if (this->GetBit(BitIndex)) {
+					SMP_msg("%zu ", BitIndex);
+				}
+			}
+		}
+	}
+	return;
+} // end of STARSBitSet::DumpBitsSet()
+
+void STARSBitSet::SetByte(const std::size_t ByteIndex, const uint8_t ByteValue) {
+	assert(ByteIndex < this->STARSBits.size());
+	this->STARSBits[ByteIndex] = ByteValue;
+	return;
+}
+
 void STARSBitSet::UnionSets(const STARSBitSet &BitSet2) {
-	size_t NumBits = this->GetNumBits();
-	assert(NumBits == BitSet2.GetNumBits());
+	assert(this->GetNumBits() == BitSet2.GetNumBits());
 
-	for (size_t index = 0; index < NumBits; ++index) {
-		if (BitSet2.GetBit(index)) {
-			this->SetBit(index);
-		}
+	for (size_t ByteIndex = 0; ByteIndex < this->STARSBits.size(); ++ByteIndex) {
+		this->STARSBits[ByteIndex] = (this->STARSBits[ByteIndex] | BitSet2.GetByte(ByteIndex));
 	}
 
 	return;
@@ -3994,11 +4022,12 @@ STARSBitSet STARSBitSetIntersection(const STARSBitSet &BitSet1, const STARSBitSe
 	assert(NumBits == BitSet2.GetNumBits());
 	STARSBitSet ReturnBitSet;
 	ReturnBitSet.AllocateBits(NumBits);
+	size_t NumBytes = (NumBits / 8);
+	if (0 != (NumBits % 8))
+		++NumBytes;
 
-	for (size_t index = 0; index < NumBits; ++index) {
-		if (BitSet1.GetBit(index) && BitSet2.GetBit(index)) {
-			ReturnBitSet.SetBit(index);
-		}
+	for (size_t ByteIndex = 0; ByteIndex < NumBytes; ++ByteIndex) {
+		ReturnBitSet.SetByte(ByteIndex, (BitSet1.GetByte(ByteIndex) & BitSet2.GetByte(ByteIndex)));
 	}
 
 	return ReturnBitSet;
@@ -4009,11 +4038,12 @@ STARSBitSet STARSBitSetUnion(const STARSBitSet &BitSet1, const STARSBitSet &BitS
 	assert(NumBits == BitSet2.GetNumBits());
 	STARSBitSet ReturnBitSet;
 	ReturnBitSet.AllocateBits(NumBits);
+	size_t NumBytes = (NumBits / 8);
+	if (0 != (NumBits % 8))
+		++NumBytes;
 
-	for (size_t index = 0; index < NumBits; ++index) {
-		if (BitSet1.GetBit(index) || BitSet2.GetBit(index)) {
-			ReturnBitSet.SetBit(index);
-		}
+	for (size_t ByteIndex = 0; ByteIndex < NumBytes; ++ByteIndex) {
+		ReturnBitSet.SetByte(ByteIndex, (BitSet1.GetByte(ByteIndex) | BitSet2.GetByte(ByteIndex)));
 	}
 
 	return ReturnBitSet;
@@ -4961,7 +4991,7 @@ unsigned int CountBitsSet(unsigned int ArgPosBits) {
 }
 
 // Utility to get highest bit set in a byte, numbered 0 (lowest) to 7 (highest).
-unsigned int HighestBitSet(unsigned char Byte) {
+unsigned int HighestBitSet(uint8_t Byte) {
 	unsigned int RetVal = 0;
 	if (Byte & 0xf0) { // check upper 4 bits
 		RetVal |= 4;  // at least bit 4 or higher is set
@@ -4975,7 +5005,7 @@ unsigned int HighestBitSet(unsigned char Byte) {
 		RetVal |= 1;
 	}
 	return RetVal;
-}
+} // end of HighestBitSet()
 
 // Utility to get lowest bit set in a byte, numbered 0 (lowest) to 7 (highest).
 unsigned int LowestBitSet(unsigned char Byte) {
@@ -5000,10 +5030,10 @@ unsigned int LowestBitSet(unsigned char Byte) {
 // Assumes that UintVal is non-zero and has some bit set.
 unsigned int HighestBitSetInUint(uint32_t UintVal) {
 	unsigned int RetVal = 0;
-	unsigned char Byte0 = UintVal & 0xff;
-	unsigned char Byte1 = UintVal & 0xff00;
-	unsigned char Byte2 = UintVal & 0xff0000;
-	unsigned char Byte3 = UintVal & 0xff000000;
+	uint8_t Byte0 = UintVal & 0xff;
+	uint8_t Byte1 = UintVal & 0xff00;
+	uint8_t Byte2 = UintVal & 0xff0000;
+	uint8_t Byte3 = UintVal & 0xff000000;
 	if (Byte3 > 0) {
 		RetVal = HighestBitSet(Byte3) + 24;
 	}
@@ -5017,7 +5047,7 @@ unsigned int HighestBitSetInUint(uint32_t UintVal) {
 		RetVal = HighestBitSet(Byte0);
 	}
 	return RetVal;
-}
+} // end of HighestBitSetInUint()
 
 
 // Initialize the FG info for the return register from any library function
diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp
index ab0f5dc95761e21c4a02e467b33dde56b1290d3d..73aa8f99fd1d51cfac8249a4b23da6e261d1b7b5 100644
--- a/src/base/SMPFunction.cpp
+++ b/src/base/SMPFunction.cpp
@@ -6721,9 +6721,12 @@ void SMPFunction::ComputeSSA(void) {
 	if (this->HasReducibleControlFlow()) {
 		this->HasStructuredCFG = (!this->HasUnresolvedIndirectJumps());
 		if (!this->HasStructuredControlFlow()) {
-			SMP_msg("ERROR: SPARK: Unstructured CFG due to unresolved indirect jumps in %s\n", this->GetFuncName());
+			SMP_msg("ERROR: SPARK: Unstructured due to unresolved indirect jumps in %s\n", this->GetFuncName());
 		}
 	}
+	else {
+		SMP_msg("ERROR: SPARK: Unstructured due to irreducible CFG in %s\n", this->GetFuncName());
+	}
 	if (DebugFlag) SMP_msg("Computing SSA renumbering.\n");
 	this->SSARenumber();
 	list<SMPBasicBlock *>::iterator BlockIter;
@@ -6860,8 +6863,11 @@ void SMPFunction::FindLoopHeadsAndTails(SMPBasicBlock *CurrBlock) {
 				set<int> DummySet;
 				DummySet.insert(FollowBlockNum);
 				this->LoopFollowNodes.push_back(DummySet);
+				map<int, STARSBitSet> DummyMap;
+				this->LoopFollowNodesReachabilitySets.push_back(DummyMap);
 				++this->LoopCount;
 				assert(this->LoopHeadBlockNumbers.size() == this->LoopCount);
+				assert(this->LoopFollowNodesReachabilitySets.size() == this->LoopCount);
 				// If this is a double tail block, we need to arrange Loop N == inner, loop N-1 == outer.
 				if (CurrBlock->IsDoubleLoopTailBlock()) {
 					OuterLoopHeadBlockNum = CurrBlock->GetOuterLoopHeaderNumberForDoubleTailBlock();
@@ -7212,12 +7218,12 @@ void
 SMPFunction::ClassifyLoop(size_t LoopNumber, int HeaderExitFollowNum, int TailExitFollowNum, SMPBasicBlock *CurrBlock, SMPBasicBlock *HeadBlock, bool HeaderBlockExitsLoop, bool TailBlockExitsLoop) {
 	this->DetectLoopFollowBlock(LoopNumber);
 	if (HeaderBlockExitsLoop && HeadBlock->HasIndirectJump()) {
-		this->HasStructuredCFG = false;
+		this->HasStructuredCFG = false; // indirect jump head loop exit
 		SMP_msg("ERROR: SPARK: Unstructured due to indirect jump head loop exit at %llx for loop %d in %s\n",
 			(uint64_t)CurrBlock->GetLastAddr(), LoopNumber, this->GetFuncName());
 	}
 	else if (TailBlockExitsLoop && CurrBlock->HasIndirectJump()) {
-		this->HasStructuredCFG = false;
+		this->HasStructuredCFG = false; // indirect jump tail loop exit 
 		SMP_msg("ERROR: SPARK: Unstructured due to indirect jump tail loop exit at %llx for loop %d in %s\n",
 			(uint64_t)CurrBlock->GetLastAddr(), LoopNumber, this->GetFuncName());
 	}
@@ -7227,7 +7233,7 @@ SMPFunction::ClassifyLoop(size_t LoopNumber, int HeaderExitFollowNum, int TailEx
 			// Conditional exits at top and bottom of loop.
 			this->LoopTypesByLoopNum[LoopNumber] = STARS_BOTTOM_TESTING_LOOP;
 			if (TailExitFollowNum != HeaderExitFollowNum) {
-				this->HasGoodLoopFollowBlocks = false; // inconsistent follow nodes, e.g. multi-level loop exit
+				this->HasGoodLoopFollowBlocks = false; // inconsistent head and tail follow nodes, e.g. multi-level loop exit
 				SMP_msg("ERROR: SPARK: Unstructured due to conflicting head and tail loop follow block nums for loop %d : %d and %d in %s\n",
 					LoopNumber, HeaderExitFollowNum, TailExitFollowNum, this->GetFuncName());
 			}
@@ -7279,6 +7285,40 @@ bool SMPFunction::DoesBlockExitLoop(std::size_t LoopNumber, SMPBasicBlock *LoopB
 	return FoundExitSuccessor;
 } // end of SMPFunction::DoesBlockExitLoop()
 
+// Populate entry in LoopFollowNodesReachabilitySets
+void SMPFunction::ComputeLoopFollowNodesReachability(const std::size_t LoopNum) {
+	// Without following back edges, record which blocks can be reached from 
+	//  each block that is the target of a loop exit (which are found in LoopFollowNodes[LoopNum]).
+	assert(LoopNum < this->GetNumLoops());
+	assert(LoopNum < this->LoopFollowNodes.size());
+	for (int FollowNodeNum : this->LoopFollowNodes[LoopNum]) {
+		STARSBitSet Reachable;
+		Reachable.AllocateBits(this->GetNumBlocks());
+		this->MarkReachableBlocks(FollowNodeNum, Reachable);
+		pair<int, STARSBitSet> MapItem(FollowNodeNum, Reachable);
+		this->LoopFollowNodesReachabilitySets[LoopNum].insert(MapItem);
+	}
+
+	return;
+} // end of SMPFunction::ComputeLoopFollowNodesReachability()
+
+// Set bits of current BlockNum and its descendants in CFG
+void SMPFunction::MarkReachableBlocks(const int BlockNum, STARSBitSet &ReachableSet) {
+	if (!ReachableSet.GetBit((size_t)BlockNum)) { // avoid looping
+		ReachableSet.SetBit((size_t)BlockNum); // Initialize to itself being reachable
+		SMPBasicBlock *CurrBlock = this->GetBlockByNum((size_t)BlockNum);
+		assert(nullptr != CurrBlock);
+		for (list<SMPBasicBlock *>::const_iterator SuccIter = CurrBlock->GetFirstConstSucc(); SuccIter != CurrBlock->GetLastConstSucc(); ++SuccIter) {
+			int SuccBlockNum = (*SuccIter)->GetNumber();
+			// Weed out back edges
+			if (!this->DoesBlockDominateBlock(SuccBlockNum, BlockNum)) {
+				this->MarkReachableBlocks(SuccBlockNum, ReachableSet);
+			}
+		}
+	}
+
+	return;
+} // end if 
 
 // Collect a set of loop-variant DEFs with the inst IDs of the DEFs.
 void SMPFunction::DetectLoopInvariantDEFs(void) {
@@ -11002,7 +11042,7 @@ void SMPFunction::FindSwitchIDom(struct SwitchTableInfo &TableInfo) {
 					// Not sure what is going on.
 					SMP_msg("ERROR: SPARK: Unstructured due to switch control flow at %llx in %s\n",
 						(uint64_t)LastAddr, this->GetFuncName());
-					this->HasStructuredCFG = false;
+					this->HasStructuredCFG = false; // Bad switch control flow
 				}
 			}
 			else if ((INDIR_JUMP == FlowType) && (PredBlock->GetNumber() == TableInfo.IndirJumpBlockNum)) {
@@ -11681,13 +11721,13 @@ bool SMPFunction::AnalyzeConditionalStatements(void) {
 						if (DistantBlockNum != FollowNodeNum) {
 							SMP_msg("ERROR: SPARK: Unstructured due to DistantBlock != FollowBlock for normal if-then at %llx in %s\n",
 								(uint64_t) LastInst->GetAddr(), this->GetFuncName());
-							this->HasStructuredCFG = false;
+							this->HasStructuredCFG = false; // DistantBlock != FollowBlock for normal if-then
 						}
 					}
 					else if (DistantBlockNum == FollowNodeNum) {
 						SMP_msg("ERROR: SPARK: Unstructured due to DistantBlock == FollowBlock for OddIfThenCase at %llx in %s\n",
 							(uint64_t) LastInst->GetAddr(), this->GetFuncName());
-						this->HasStructuredCFG = false;
+						this->HasStructuredCFG = false; // DistantBlock == FollowBlock for OddIfThenCase
 					}
 				}
 				else {
@@ -11938,7 +11978,7 @@ int SMPFunction::FindConditionalFollowNode(int HeadBlockNum) {
 #if 0
 								SMP_msg("WARNING: Inconsistent loop-back HeadBlockNums for conditional block %d in func at %llx\n",
 									HeadBlockNum, (uint64_t) this->GetFirstFuncAddr());
-								this->HasStructuredCFG = false;  // irrecoverable problem
+								this->HasStructuredCFG = false;  // Inconsistent loop head block nums; irrecoverable problem
 								return SMP_BLOCKNUM_UNINIT;
 #else
 								LoopBackCounter = 0;
@@ -16725,7 +16765,7 @@ void SMPFunction::UpdateLoopFollowBlockNum(int LoopHeadBlockNum, int FollowBlock
 	else if (OldFollowNum != FollowBlockNum) {
 		if (SMP_BLOCKNUM_UNINIT == FollowBlockNum) {
 			if (this->HasGoodLoopFollowBlocks) {
-				this->HasGoodLoopFollowBlocks = false;
+				this->HasGoodLoopFollowBlocks = false; // conflicting loop follow block nums
 				SMP_msg("ERROR: SPARK: Unstructured due to conflicting loop follow block nums for loop %d : %d and %d in %s\n",
 					LoopNum, OldFollowNum, FollowBlockNum, this->GetFuncName());
 			}
@@ -16752,7 +16792,7 @@ void SMPFunction::UpdateLoopFollowBlockNum(int LoopHeadBlockNum, int FollowBlock
 			}
 			if (!success) {
 				if (this->HasGoodLoopFollowBlocks) {
-					this->HasGoodLoopFollowBlocks = false;
+					this->HasGoodLoopFollowBlocks = false; // Conflicting loop follow blocks
 					SMP_msg("ERROR: SPARK: Unstructured due to conflicting loop follow block nums for loop %d : %d and %d in %s\n",
 						LoopNum, OldFollowNum, FollowBlockNum, this->GetFuncName());
 					if (VerboseOutput)
@@ -16760,6 +16800,7 @@ void SMPFunction::UpdateLoopFollowBlockNum(int LoopHeadBlockNum, int FollowBlock
 					this->DumpDotCFG();
 				}
 			}
+			this->LoopFollowNodes[LoopNum].insert(FollowBlockNum);
 		}
 	}
 	return;
@@ -16980,7 +17021,7 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 	//  to be identified as a JUMP_TO_DEFAULT_CASE (which is not part of the Cifuentes analysis scheme), we 
 	//  do the loop analysis before the switch analysis.
 	if (this->HasStructuredControlFlow() && this->HasUnresolvedIndirectJumps()) { // redundant ???
-		this->HasStructuredCFG = false;
+		this->HasStructuredCFG = false; // Unresolved indirect jump
 	}
 
 
@@ -17013,13 +17054,13 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 				if (CurrInst->IsLoopExitStatement(InvertedExit)) {
 					STARS_ea_t JumpTarget = CurrInst->GetJumpTarget();
 					if ((STARS_BADADDR == JumpTarget) || (!this->IsInstIDInFunc(JumpTarget))) {
-						this->HasStructuredCFG = false;
+						this->HasStructuredCFG = false; // Bad jump target
 						SMP_msg("ERROR: SPARK: Unstructured due to bad jump target at %llx in %s\n", (uint64_t) InstAddr, this->GetFuncName());
 						break; // no point in continuing if we cannot translate to SPARK Ada
 					}
 
 					if (this->FindMultiLoopContinue((int) BlockIndex)) {
-						this->HasStructuredCFG = false;
+						this->HasStructuredCFG = false; // Multi-loop continue
 						break; // no point in continuing if we cannot translate to SPARK Ada
 					}
 
@@ -17110,7 +17151,7 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 					STARS_ea_t JumpTarget = CurrInst->GetJumpTarget();
 					if ((STARS_BADADDR == JumpTarget) || (!this->IsInstIDInFunc(JumpTarget))) {
 						SMP_msg("ERROR: SPARK: Unstructured due to bad jump target at %llx in %s\n", (uint64_t) InstAddr, this->GetFuncName());
-						this->HasStructuredCFG = false;
+						this->HasStructuredCFG = false; // Bad jump target
 						break; // no point in continuing if we cannot translate to SPARK Ada
 					}
 					else {
@@ -17142,9 +17183,14 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 
 	if (global_STARS_program->ShouldSTARSTranslateToSPARKAda()) {
 		if (!this->HasGoodLoopFollowBlocks) {
-			this->HasStructuredCFG = false;
+			this->HasStructuredCFG = false; // Bad loop follow blocks
 			SMP_msg("ERROR: SPARK: Function %s declared unstructured because of bad loop follow blocks.\n",
 				this->GetFuncName());
+			for (size_t LoopNum = 0; LoopNum < this->GetNumLoops(); ++LoopNum) {
+				if (1 < this->LoopFollowNodes[LoopNum].size()) {
+					this->ComputeLoopFollowNodesReachability(LoopNum);
+				}
+			}
 		}
 
 		if (!StartupFunc) {
@@ -17155,7 +17201,7 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 					if (CurrBlock->HasIndirectJump()) {
 						bool StructuredSwitch = this->AnalyzeSwitchStatement(CurrBlock);
 						if (!StructuredSwitch) {
-							this->HasStructuredCFG = false;
+							this->HasStructuredCFG = false; // Unstructured switch
 							SMP_msg("ERROR: SPARK: Unstructured switch statements in %s\n", this->GetFuncName());
 							break; // give up as soon as CFG is unstructured
 						}
@@ -17168,7 +17214,7 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 			if (this->HasStructuredControlFlow()) {
 				bool StructuredConditionals = this->AnalyzeConditionalStatements();
 				if (!StructuredConditionals) {
-					this->HasStructuredCFG = false;
+					this->HasStructuredCFG = false; // Unstructured conditionals
 					SMP_msg("ERROR: SPARK: Unstructured COND_BRANCH statements in %s\n", this->GetFuncName());
 #if 0
 					this->Dump();
@@ -17273,7 +17319,7 @@ void SMPFunction::MarkLoopContinueCases(const SMPBasicBlock *CurrBlock, const in
 		else if (this->FindLoopContinuePattern((int)BlockIndex)) {
 			SMP_msg("WARNING: SPARK: LOOP_CONTINUE case detected in block %d FollowBlock %d of %s\n",
 				CurrBlock->GetNumber(), FollowBlockNum, this->GetFuncName());
-			this->HasStructuredCFG = false;
+			this->HasStructuredCFG = false; // loop continue detected
 			this->DumpDotCFG();
 			this->SetControlFlowType(InstAddr, LOOP_CONTINUE);
 		}
@@ -17289,7 +17335,7 @@ void SMPFunction::MarkLoopContinueCases(const SMPBasicBlock *CurrBlock, const in
 	}
 	else {
 		// Fall-through to next function, probably IDA Pro problem in func ID.
-		this->HasStructuredCFG = false;
+		this->HasStructuredCFG = false; // fall-through to next func
 		SMP_msg("ERROR: SPARK: Unstructured due to fall-through from %llx is not in function %s\n",
 			(uint64_t)InstAddr, this->GetFuncName());
 	}
@@ -18845,14 +18891,18 @@ void SMPFunction::Dump(void) {
 			}
 			if (!this->LoopFollowNodes.empty()) {
 				int FollowBlockNum = SMP_BLOCKNUM_UNINIT;
-				bool MultiExitLoop = (1 < this->LoopFollowNodes.size());
+				bool MultiExitLoop = (1 < this->LoopFollowNodes[LoopNum].size());
 				if (!MultiExitLoop) {
 					SMP_msg(" Follow block number: %d", *(this->LoopFollowNodes[LoopNum].cbegin()));
 				}
 				else {
-					SMP_msg(" Follow block numbers: ");
+					SMP_msg(" Follow block numbers: \n");
 					for (int FollowBlockNum : this->LoopFollowNodes[LoopNum]) {
 						SMP_msg("%d ", FollowBlockNum);
+						SMP_msg("Reachable descendants: ");
+						const STARSBitSet &CurrBitSet = this->LoopFollowNodesReachabilitySets[LoopNum][FollowBlockNum];
+						CurrBitSet.DumpBitsSet();
+						SMP_msg("\n");
 					}
 				}
 			}
@@ -19539,7 +19589,7 @@ void SMPFunction::PreProcessForSPARKAdaTranslation(void) {
 		SMPInstr *LastInst = (*LastInstIter);
 		if (LastInst->IsBranchToOtherFunc()) {
 			SMP_msg("SPARK: WARNING: Bad CFG (branch outside function at %llx) \n", (uint64_t)LastInst->GetAddr());
-			this->HasStructuredCFG = false;
+			this->HasStructuredCFG = false; // branch outside func
 		}
 
 		if (HasLoops && CurrBlock->HasMemoryWrite() && this->IsBlockInAnyLoop((int) BlockNum)) {
diff --git a/src/base/SMPProgram.cpp b/src/base/SMPProgram.cpp
index 66120633a12521b0c73302a1ddab347d0cddb702..bd6c97b5b1283b4b00ed74d7d00e709d34497933 100644
--- a/src/base/SMPProgram.cpp
+++ b/src/base/SMPProgram.cpp
@@ -1160,12 +1160,25 @@ bool SMPProgram::EmitProgramSPARKAda(void) {
 			if (!TempFunc->IsLinkerStub()) {
 				SMP_msg("WARNING: No SPARK Ada translation due to Unstructured control flow for func %s at %llx\n",
 					TempFunc->GetFuncName(), (uint64_t)TempFunc->GetFirstFuncAddr());
+				if (!TempFunc->HasGoodRTLs()) {
+					SMP_msg("ERROR: SPARK: Unstructured due to bad RTLs for func %s at %llx\n",
+						TempFunc->GetFuncName(), (uint64_t)TempFunc->GetFirstFuncAddr());
+				}
+				else if (!TempFunc->StackPtrAnalysisSucceeded()) {
+					SMP_msg("ERROR: SPARK: Unstructured due to stack ptr analysis for func %s at %llx\n",
+						TempFunc->GetFuncName(), (uint64_t)TempFunc->GetFirstFuncAddr());
+				}
+				else if (TempFunc->HasUnresolvedIndirectJumps()) {
+					SMP_msg("ERROR: SPARK: Unstructured due to unresolved indirect jumps for func %s at %llx\n",
+						TempFunc->GetFuncName(), (uint64_t)TempFunc->GetFirstFuncAddr());
+				}
 
 				// Emit minimal stub
 				SMP_fprintf(SpecFile, "procedure %s with\n", TempFunc->GetFuncName());
 				SMP_fprintf(SpecFile, "\tGlobal => (In_Out => X86.RSP),\n");
 				SMP_fprintf(SpecFile, "\tPost => (X86.RSP = X86.RSP'Old + 8);\n\n");
 				SMP_fprintf(BodyFile, "-- Minimal stub emitted due to unstructured control flow.\n");
+				SMP_fprintf(BodyFile, "-- Starting code address was %llx\n", (uint64_t)TempFunc->GetFirstFuncAddr());
 				SMP_fprintf(BodyFile, "procedure %s is\nbegin\n\tX86.RSP := X86.RSP + %u;\n", TempFunc->GetFuncName(), ByteWidth);
 				SMP_fprintf(BodyFile, "end %s;\n\n", TempFunc->GetFuncName());