diff --git a/include/base/SMPFunction.h b/include/base/SMPFunction.h
index 997b69b17d6dafb699ab1b309818e8e0b53f37bc..112e3558caad3782b2b64c6cf34445c2085d389a 100644
--- a/include/base/SMPFunction.h
+++ b/include/base/SMPFunction.h
@@ -1036,6 +1036,7 @@ private:
 	int TrackConditionalBranchTerminus(int BranchHeadBlockNum, int CurrBlockNum, STARSBitSet &BlocksSeen, int &BlockAlreadySeenCounter); // Track CurrBlockNum until we reach block that BranchHeadBlockNum doesn't dominate, or dead end. Return block num, possibly SMP_BLOCKNUM_COMMON_RETURN.
 	bool FindUnstructuredIfThenElse(const int HeadBlockNum, const int ThenBlockNum, const int ElseBlockNum, const int FollowBlockNum) const; // Do IF and ELSE branches merge before FollowBlockNum?
 	bool FindMultiLoopContinue(const int BranchBlockNum); // Does COND_BRANCH behave as an unstructured multi-level loop continue statement?
+	bool DetectConditionalReachabilityErrors(const int HeadBlockNum, const int FTBlockNum, const int NFTBlockNum, const STARSBitSet &FTBlocksSeen, const STARSBitSet &NFTBlocksSeen, const STARSBitSet &CommonBlocksSeen);
 	void FindGuardedLoops(void); // Find guarded loops and fill the GuardToLoopMap and LoopToGuardMap
 
 	bool IsSPARKLoopInTranslationStack(void) const; // Are we already translating a SPARK_LOOP when we encounter another loop?
diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp
index fdcd719add988d8f4c25816b20908e4d3d35aeb4..481c8f4c6f3f814722499398e9285fd09df95fb7 100644
--- a/src/base/SMPFunction.cpp
+++ b/src/base/SMPFunction.cpp
@@ -7406,7 +7406,11 @@ void SMPFunction::ComputeLoopFollowNodesReachability(const std::size_t LoopNum)
 // Set bits of current BlockNum and its descendants in CFG that are dominated by LoopHeadBlockNum
 // NOTE: LoopHeadBlockNum can be any dominating block num, with LoopNum < 0 indicating we are not in a loop.
 void SMPFunction::MarkReachableBlocks(const int BlockNum, const int LoopNum, const int LoopHeadBlockNum, STARSBitSet &ReachableSet) {
-	if (!ReachableSet.GetBit((size_t)BlockNum)) { // avoid looping and duplication of work
+	bool ProperDominance = true;
+#if 1
+	ProperDominance = this->DoesBlockDominateBlock(LoopHeadBlockNum, BlockNum);
+#endif
+	if ((!ReachableSet.GetBit((size_t)BlockNum)) && ProperDominance) { // avoid looping and duplication of work
 		ReachableSet.SetBit((size_t)BlockNum); // Initialize to itself being reachable
 		SMPBasicBlock *CurrBlock = this->GetBlockByNum((size_t)BlockNum);
 		assert(nullptr != CurrBlock);
@@ -12077,12 +12081,14 @@ int SMPFunction::FindConditionalFollowNode(int HeadBlockNum) {
 		else {
 			SMP_msg("INFO: SPARK: Failure on old version, success on new version of FindConditionalFollowNode at block %d Follow: %d ", HeadBlockNum, NewAlgorithmFollowNode);
 			ReturnFollowBlockNum = NewAlgorithmFollowNode;
+			this->DumpDotCFG();
 		}
 	}
 	else {
 		if (BadNew) {
 			SMP_msg("INFO: SPARK: Success on old version, failure on new version of FindConditionalFollowNode at block %d Follow: %d ", HeadBlockNum, OldAlgorithmFollowNode);
 			ReturnFollowBlockNum = OldAlgorithmFollowNode;
+			this->DumpDotCFG();
 		}
 		else {
 			SMP_msg("INFO: SPARK: Success on both versions of FindConditionalFollowNode at block %d ", HeadBlockNum);
@@ -12545,9 +12551,11 @@ int SMPFunction::FindConditionalFollowNode3(int HeadBlockNum) {
 
 	STARS_ea_t HeadLastAddr = HeadBlock->GetLastAddr();
 	bool HeadBlockIsInALoop = this->IsBlockInAnyLoop(HeadBlockNum);
+
+	// LastCFType is incomplete at this point, as the current method is part
+	//  of the analysis. But SHORT_CIRCUIT_BRANCH locations have already been detected.
 	ControlFlowType LastCFType = this->GetControlFlowType(HeadLastAddr);
 	int InnerMostLoopNum = HeadBlockIsInALoop ? this->GetInnermostLoopNum(HeadBlockNum) : -1;
-
 	bool ShortCircuit = (IsShortCircuitFlow(LastCFType));
 
 	assert(2 == HeadBlock->GetNumSuccessors());
@@ -12615,21 +12623,45 @@ int SMPFunction::FindConditionalFollowNode3(int HeadBlockNum) {
 	bool DominanceProblem = (FTNotDominated || NFTNotDominated);
 	bool Case0 = false;
 
+	// Find CFG problems that are obvious just from the reachability bitsets.
+	if (this->DetectConditionalReachabilityErrors(HeadBlockNum, FTBlockNum, NFTBlockNum, FTBlocksSeen, NFTBlocksSeen, CommonBlocksSeen)) {
+		return FollowBlockNum; // error; still set to SMP_BLOCKNUM_UNINIT
+	}
+
 	// Based on CommonBlocksCount, FirstCommonBlockNum, FTBlockNum, and NFTBlockNum, we
 	//  can find which case in the comment above applies.
 	if (0 == CommonBlocksCount) { // Case 1 or Case 0.
-		FollowBlockNum = SMP_BLOCKNUM_COMMON_RETURN;
-		// Detect the exception subcase.
-		SMPBasicBlock *LastFTBlockReached = this->GetBlockByNum((size_t)LastFTReachableBlockNum);
-		SMPBasicBlock *LastNFTBlockReached = this->GetBlockByNum((size_t)LastNFTReachableBlockNum);
-		if ((1 == LastFTBlockReached->GetNumSuccessors()) && (1 == LastNFTBlockReached->GetNumSuccessors())) {
-			int NextFTBlockNum = (*(LastFTBlockReached->GetFirstConstSucc()))->GetNumber();
-			int NextNFTBlockNum = (*(LastNFTBlockReached->GetFirstConstSucc()))->GetNumber();
-			bool NotLoopBack = (NextFTBlockNum > HeadBlockNum);
-			if ((NextFTBlockNum == NextNFTBlockNum) && NotLoopBack) { // Exception to Case 1
-				FollowBlockNum = NextFTBlockNum;
+		FollowBlockNum = SMP_BLOCKNUM_COMMON_RETURN; // Case 1
+
+		// Detect the Case 1 exception subcase.
+		int NextFTBlockNum = SMP_BLOCKNUM_UNINIT;
+		int NextNFTBlockNum = SMP_BLOCKNUM_UNINIT;
+		if (0 <= LastFTReachableBlockNum) { // FTBlock was dominated by HeadBlock
+			SMPBasicBlock *LastFTBlockReached = this->GetBlockByNum((size_t)LastFTReachableBlockNum);
+			if (1 == LastFTBlockReached->GetNumSuccessors()) {
+				NextFTBlockNum = (*(LastFTBlockReached->GetFirstConstSucc()))->GetNumber();
+			}
+		}
+		else { // FTBlock was outside region dominated by HeadBlock
+			NextFTBlockNum = FTBlockNum; // First block outside dominated region
+			IfThenElseCase = false;
+		}
+		if (0 <= LastNFTReachableBlockNum) { // FTBlock was dominated by HeadBlock
+			SMPBasicBlock *LastNFTBlockReached = this->GetBlockByNum((size_t)LastNFTReachableBlockNum);
+			if (1 == LastNFTBlockReached->GetNumSuccessors()) {
+				NextNFTBlockNum = (*(LastNFTBlockReached->GetFirstConstSucc()))->GetNumber();
 			}
 		}
+		else { // FTBlock was outside region dominated by HeadBlock
+			NextNFTBlockNum = NFTBlockNum; // First block outside dominated region
+			IfThenElseCase = false;
+		}
+
+		bool NotLoopBack = (NextFTBlockNum > HeadBlockNum);
+		if ((NextFTBlockNum == NextNFTBlockNum) && NotLoopBack) { // Exception to Case 1
+			FollowBlockNum = NextFTBlockNum;
+		}
+
 		if (FollowBlockNum == SMP_BLOCKNUM_COMMON_RETURN) { // Not the exception to Case 1; search for Case 0.
 			if (HeadBlockIsInALoop && DominanceProblem) { // Maybe one COND_BRANCH successor is our own loop head.
 				SMPBasicBlock *NFTBlock = this->GetBlockByNum((size_t)NFTBlockNum);
@@ -13002,6 +13034,80 @@ bool SMPFunction::FindMultiLoopContinue(const int BranchBlockNum) {
 	return Unstructured;
 } // end of SMPFunction::FindMultiLoopContinue()
 
+// Detect conditional statement structuring errors that are obvious just from the reachability bitsets.
+bool SMPFunction::DetectConditionalReachabilityErrors(const int HeadBlockNum, const int FTBlockNum, const int NFTBlockNum, const STARSBitSet &FTBlocksSeen, const STARSBitSet &NFTBlocksSeen, const STARSBitSet &CommonBlocksSeen) {
+	bool Unstructured = false;
+
+	// All blocks reachable by either FTBlock or NFTBlock should either precede the intersection point or
+	//  should be in CommonBlocksSeen (i.e. RPO block number greater than intersection point RPO number
+	//  should imply that we are merely continuing downward from the intersection point).
+	int IntersectionBlockNum = CommonBlocksSeen.FindLowestBitSet();
+	bool TracesIntersect = (0 < IntersectionBlockNum);
+	if (TracesIntersect) {
+		for (size_t BlockNum = (size_t)(IntersectionBlockNum + 1); BlockNum < this->GetNumBlocks(); ++BlockNum) {
+			if (FTBlocksSeen.GetBit(BlockNum)) {
+				bool success = NFTBlocksSeen.GetBit(BlockNum);
+				if (!success) {
+					Unstructured = true;
+					break;
+				}
+			}
+		}
+	}
+	if (!Unstructured) {
+		// Ensure that any loop contained inside the then or else clauses has its exit target
+		//  blocks dominated by the loop head block; a "back door" into a loop exit target block
+		//  that does not come from the loop must be restructured.
+		int LowestBlockSeen = FTBlocksSeen.FindLowestBitSet();
+		int HighestBlockSeen = FTBlocksSeen.FindHighestBitSet();
+		int LimitBlockNum = TracesIntersect ? IntersectionBlockNum : HighestBlockSeen;
+		if (0 <= LowestBlockSeen) {
+			for (int BlockNum = LowestBlockSeen; BlockNum <= LimitBlockNum; ++BlockNum) {
+				if (FTBlocksSeen.GetBit((size_t)BlockNum)) {
+					SMPBasicBlock *CurrBlock = this->GetBlockByNum((size_t)BlockNum);
+					if (CurrBlock->IsLoopHeaderBlock()) {
+						int LoopNum = this->GetLoopNumFromHeaderBlockNum(BlockNum);
+						assert(0 <= LoopNum);
+						for (int ExitTargetBlockNum : this->LoopExitTargets[(size_t)LoopNum]) {
+							if (!this->DoesBlockDominateBlock(HeadBlockNum, ExitTargetBlockNum)) {
+								Unstructured = true;
+								break;
+							}
+						}
+					}
+				}
+			}
+		}
+	}
+	if (!Unstructured) {
+		// Ensure that any loop contained inside the then or else clauses has its exit target
+		//  blocks dominated by the loop head block; a "back door" into a loop exit target block
+		//  that does not come from the loop must be restructured.
+		int LowestBlockSeen = NFTBlocksSeen.FindLowestBitSet();
+		int HighestBlockSeen = NFTBlocksSeen.FindHighestBitSet();
+		int LimitBlockNum = TracesIntersect ? IntersectionBlockNum : HighestBlockSeen;
+		if (0 <= LowestBlockSeen) {
+			for (int BlockNum = LowestBlockSeen; BlockNum <= LimitBlockNum; ++BlockNum) {
+				if (NFTBlocksSeen.GetBit((size_t)BlockNum)) {
+					SMPBasicBlock *CurrBlock = this->GetBlockByNum((size_t)BlockNum);
+					if (CurrBlock->IsLoopHeaderBlock()) {
+						int LoopNum = this->GetLoopNumFromHeaderBlockNum(BlockNum);
+						assert(0 <= LoopNum);
+						for (int ExitTargetBlockNum : this->LoopExitTargets[(size_t)LoopNum]) {
+							if (!this->DoesBlockDominateBlock(HeadBlockNum, ExitTargetBlockNum)) {
+								Unstructured = true;
+								break;
+							}
+						}
+					}
+				}
+			}
+		}
+	}
+
+	return Unstructured;
+} // end of SMPFunction::DetectConditionalReachabilityErrors()
+
 // Find guarded loops and fill the GuardToLoopMap and LoopToGuardMap
 void SMPFunction::FindGuardedLoops(void) {
 	assert(this->HasStructuredControlFlow());
@@ -14156,17 +14262,20 @@ int SMPFunction::FindLastBlockProcessedInChain(const int StartingBlockNum) const
 	SMPBasicBlock *StartingBlock = this->GetBlockByNum((size_t) StartingBlockNum);
 	assert(StartingBlock->IsProcessed());
 
-	for (list<SMPBasicBlock *>::const_iterator SuccIter = StartingBlock->GetFirstConstSucc();
-		SuccIter != StartingBlock->GetLastConstSucc();
-		++SuccIter) {
-		SMPBasicBlock *SuccBlock = (*SuccIter);
-		if (SuccBlock->IsProcessed()) {
-			int SuccBlockNum = SuccBlock->GetNumber();
-			if (SuccBlockNum <= StartingBlockNum) // back edge
-				continue;
-			int TempHighestFound = this->FindLastBlockProcessedInChain(SuccBlockNum);
-			if (HighestRPOBlockFound < TempHighestFound)
-				HighestRPOBlockFound = TempHighestFound;
+	if (!StartingBlock->IsSCCPVisited()) {
+		StartingBlock->SetSCCPVisited(true);
+		for (list<SMPBasicBlock *>::const_iterator SuccIter = StartingBlock->GetFirstConstSucc();
+			SuccIter != StartingBlock->GetLastConstSucc();
+			++SuccIter) {
+			SMPBasicBlock *SuccBlock = (*SuccIter);
+			if (SuccBlock->IsProcessed()) {
+				int SuccBlockNum = SuccBlock->GetNumber();
+				if (SuccBlockNum <= StartingBlockNum) // back edge
+					continue;
+				int TempHighestFound = this->FindLastBlockProcessedInChain(SuccBlockNum);
+				if (HighestRPOBlockFound < TempHighestFound)
+					HighestRPOBlockFound = TempHighestFound;
+			}
 		}
 	}
 
@@ -24109,6 +24218,7 @@ void SMPFunction::EmitSPARKAdaForConditional(int HeaderBlockNum, int FollowBlock
 	}
 #if 1
 	else if (InsideLoop) {
+		this->ResetSCCPVisitedBlocks(); // prune search in FindLastBlockProcessedInChain()
 		int LastBlockEmittedNum = this->FindLastBlockProcessedInChain(HeaderBlockNum);
 		SMPBasicBlock *LastBlockEmitted = this->GetBlockByNum((size_t) LastBlockEmittedNum);
 		assert(nullptr != LastBlockEmitted);