diff --git a/include/base/SMPBasicBlock.h b/include/base/SMPBasicBlock.h
index ada394406ef392128f740ced5e54df0cd19868e5..2d4f46b527525a51c1550b997ec15c75eea401f1 100644
--- a/include/base/SMPBasicBlock.h
+++ b/include/base/SMPBasicBlock.h
@@ -234,7 +234,6 @@ public:
 	std::vector<SMPInstr *>::const_reverse_iterator GetInstConstRevIterFromAddr(STARS_ea_t InstAddr) const;
 	inline SMPInstr *GetInstFromIndex(size_t VecIndex) const { return InstVec.at(VecIndex); };
 	size_t GetIndexFromInstAddr(STARS_ea_t InstAddr) const; // Get the InstVec index for the instruction at InstAddr. Assert if not found.
-	SMPInstr *FindBranchCompareOrTest(SMPoperator &BranchOperator, STARS_ea_t &DecAddr, bool SearchCase, int FlagsSSANum); // Find the compare or test that sets the flags used in COND_BRANCH at end of block, else NULL; If decrement found instead, fill DecAddr
 	STARS_sval_t GetIncomingStackDelta(void) const { return (*(GetFirstConstInst()))->GetStackPtrOffset(); };
 	inline STARS_sval_t GetOutgoingStackDelta(void) const { return OutgoingStackDelta; };
 	ControlFlowType GetLastInstCFType(void) const;  // Get the enum ControlFlowType for the last inst
@@ -413,6 +412,7 @@ public:
 	std::size_t GetNumSuccessorsMinusBackEdges(void) const; // Compute successor count, excluding loop-back edges.
 	int GetFirstNonBackEdgeSuccNum(void) const; // Avoid back edges; get first SuccBlockNum that is not back edge.
 	bool DoesBlockExitLoop(void) const; // block ends with LOOP_EXIT of some kind?
+	SMPInstr *FindBranchCompareOrTest(SMPoperator &BranchOperator, STARS_ea_t &DecAddr, bool SearchCase, int FlagsSSANum); // Find the compare or test that sets the flags used in COND_BRANCH at end of block, else NULL; If decrement found instead, fill DecAddr
 	STARS_ea_t GetUltimateOperandSource(STARS_ea_t UseAddr, const STARSOpndTypePtr &UseOp, int UseSSANum); // trace through move and Phi defs to some defining operation.
 	bool GetUltimateInitValue(const STARSOpndTypePtr &UseOp, STARS_ea_t InstAddr, int SSANum, bool LocalName, STARSOpndTypePtr &DefMoveOp, STARS_uval_t &InitValue);
 		// Trace back to const or InArg with min const value; follow Phi USEs to before-loop locations only.
diff --git a/include/base/SMPDataFlowAnalysis.h b/include/base/SMPDataFlowAnalysis.h
index ecb88e94176b3cbb9cf5a4491ae71286e57ac9f8..508f8aa06395ad823bb6d43efa96dccdaaca296c 100644
--- a/include/base/SMPDataFlowAnalysis.h
+++ b/include/base/SMPDataFlowAnalysis.h
@@ -806,6 +806,7 @@ private:
 
 typedef std::set<DefOrUse, LessDefUse> STARSDefUseSet;
 typedef std::set<DefOrUse, LessDefUse>::iterator STARSDefUseIter;
+typedef std::set<DefOrUse, LessDefUse>::const_iterator STARSDefUseConstIter;
 typedef std::vector<DefOrUse>::iterator DefUseListIter;
 
 // A data or function pointer shadowing point is a code address paired with an index
diff --git a/include/base/SMPFunction.h b/include/base/SMPFunction.h
index 47beb4e74f74316f4f7270d26f053349538d816d..bcb41b2cf70f53c904cc0e82ef0ad09e19e24170 100644
--- a/include/base/SMPFunction.h
+++ b/include/base/SMPFunction.h
@@ -170,6 +170,15 @@ enum SPARKTranslationCFType {
 #define STARS_BOTTOM_TESTING_LOOP 2
 #define STARS_INFINITE_OR_MIDDLE_TESTING_LOOP 3
 #define STARS_CONSTANT_ITERATIONS_TOP_TESTING_LOOP 4
+#define STARS_TOP_AND_BOTTOM_TESTING_LOOP 5
+
+inline bool DoesLoopTestAtTop(const int LoopType) {
+	return ((STARS_TOP_TESTING_LOOP == LoopType) || (STARS_TOP_AND_BOTTOM_TESTING_LOOP == LoopType) || (STARS_CONSTANT_ITERATIONS_TOP_TESTING_LOOP == LoopType));
+}
+
+inline bool DoesLoopTestAtBottom(const int LoopType) {
+	return ((STARS_BOTTOM_TESTING_LOOP == LoopType) || (STARS_TOP_AND_BOTTOM_TESTING_LOOP == LoopType));
+}
 
 // A struct used to describe the comparison used to exit a loop or loop back.
 //  For loops that could not be analyzed, CompareOperator is SMP_NULL_OPERATOR.
@@ -225,6 +234,14 @@ struct InductionVarFamily {
 typedef std::list<struct InductionVarFamily> STARSInductionVarFamilyList;
 typedef STARSInductionVarFamilyList::iterator STARSInductionVarFamilyIter;
 
+struct LoopExitingBlockInfo {
+	int ExitingBlockNum; // Block # within loop that exits the loop
+	int TargetBlockNum;  // Block # branched to outside the loop
+	SMPInstr *CompareTestDecInst; // The compare, test, or decrement instruction that sets flags used by the COND_BRANCH to exit.
+	bool ShortCircuitExpr; // COND_BRANCH is part of a short circuit expression
+	bool ReferencesBIV; // CompareTestDecInst references a BIV for this loop
+};
+
 // triple: memory write expr, ByteWidth, index into vector of stack pointer copy InstAddrs
 typedef std::list<std::pair<STARSExprSetIter, std::pair<std::size_t, int> > > STARSMemWriteExprsList;
 typedef STARSMemWriteExprsList::iterator STARSMemWriteExprListIter;
@@ -420,16 +437,17 @@ public:
 	inline void SetReturnAddressStatus(FuncType funcType) {
 		ReturnAddrStatus = funcType;
 	}
-	inline void SetFuncProcessed(bool Status) { FuncProcessed = Status; return; };
+	inline void SetFuncProcessed(bool Status) { FuncProcessed = Status; };
 	inline void SetHasIndirectCalls(void) { IndirectCalls = true; };
 	inline void SetHasUnresolvedIndirectCalls(void) { UnresolvedIndirectCalls = true; };
+	void SetHasUnstructuredCFG(void);
 	inline void SetHasSystemCalls(void) { SystemCalls = true; };
 	inline void SetAltersSPARKMemory(void) { AltersMemory = true; };
-	inline void SetFuncSafe(bool Status) { SafeFunc = Status; return; };
-	inline void SetSpecFuncSafe(bool Status) { SpecSafeFunc = Status; return; };
-	inline void SetNeedsFrame(bool Status) { NeedsStackReferent = Status; return; };
-	inline void SetSpecNeedsFrame(bool Status) { SpecNeedsStackReferent = Status; return; };
-	inline void SetUnsafeForFastReturns(bool Status, UnsafeFastReturnReason Reason) { UnsafeForFastReturns = Status; FastReturnStatus |= (int) Reason; return; };
+	inline void SetFuncSafe(bool Status) { SafeFunc = Status; };
+	inline void SetSpecFuncSafe(bool Status) { SpecSafeFunc = Status; };
+	inline void SetNeedsFrame(bool Status) { NeedsStackReferent = Status; };
+	inline void SetSpecNeedsFrame(bool Status) { SpecNeedsStackReferent = Status; };
+	inline void SetUnsafeForFastReturns(bool Status, UnsafeFastReturnReason Reason) { UnsafeForFastReturns = Status; FastReturnStatus |= (int) Reason; };
 	inline void SetIsSpeculative(bool IsS) { IsSpeculative = IsS; };
 	inline void SetIsMutuallyRecursive(void) { MutuallyRecursive = true; };
 	inline void SetIsCalledFromOrphanedCode(void) { CalledFromOrphanCode = true; };
@@ -524,6 +542,7 @@ public:
 	inline bool IsOddIfThenBranch(const int BranchBlockNum) const { return (OddIfThenBranches.cend() != OddIfThenBranches.find(BranchBlockNum)); };
 	inline bool UsesFramePointer(void) const { return UseFP; };
 	inline bool FuncHasHashingCode(void) const { return HasHashingCode; };
+	inline bool HasShortCircuitConditional(void) const { return HasShortCircuitExpr; };
 	inline bool HasGoodFGStackTable(void) const { return (!(NegativeOffsetFineGrainedStackTable.empty())); };
 	bool IsLiveIn(const STARSOpndTypePtr &CurrOp) const;
 	inline bool IsLiveOut(const STARSOpndTypePtr &CurrOp) const {
@@ -631,6 +650,7 @@ public:
 	void BuildLoopList(int BlockNum, std::list<std::size_t> &LoopList) const; // build list of loop numbers that BlockNum is part of.
 	void BuildLoopBlockList(const size_t LoopNum, std::list<std::size_t> &BlockList); // build list of Block numbers contained in LoopNum.
 	void BuildBlockListFromBitset(const STARSBitSet &CurrBitSet, std::list<std::size_t> &BlockList) const; // each bit set in CurrBitSet is a block # for BlockList
+	void BuildLoopIterationCountExprs(const bool VerboseOutput, FILE *InfoAnnotFile); // Fill in LoopIterationsCountExprs[each LoopIndex]; emit SENTINEL annotations
 	void AnalyzeLoopIterations(void); // analyze how many times each loop iterates
 	STARSExpression *CreateMemoryAddressExpr(const STARSOpndTypePtr &MemDefOp, SMPInstr *WriteInst); // create expression for the memory address computation in MemDefOp
 	void AliasAnalysis(void); // Find memory writes with possible aliases
@@ -656,6 +676,7 @@ public:
 	bool IsDefUsedInUnsafeMemWrite(STARSOpndTypePtr DefOp, int DefSSANum, STARS_ea_t DefAddr); // Is Defop+DefSSANum at DefAddr used as address reg or as source operand in unsafe memory write?
 	bool IsAddressRegSafe(const STARSOpndTypePtr &UseOp, STARS_ea_t UseAddr, int UseSSANum); // Is UseOp+UseSSANum at UseAddr a safe write?
 	void MarkFunctionSafe(void); // Does analysis to see if the function can be marked safe
+	void MarkSpecialNumericErrorCases(void); // Detect and mark special cases before emitting numeric error annotations.
 	void FreeUnusedMemory2(void); // After loop 2 in SMPProgram::Analyze(), free memory
 	void FreeUnusedMemory3(void); // After loop 3 in SMPProgram::Analyze(), free memory
 	void FreeUnusedMemory4(void); // After loop 4 (type inference) in SMPProgram::Analyze(), free memory
@@ -724,6 +745,7 @@ private:
 	bool StackFrameExtendsPastStackTop; // Locals are accessed from unallocated space beyond the top of stack.
 	bool IsSpeculative;	    // Have we started the speculative portion of the analysis for this function.
 	bool HasHashingCode; // Has apparent hashing or crypto code that intentionally overflows.
+	bool HasShortCircuitExpr; // Has at least one short circuit conditional expression.
 	bool HasInArgCodePointer; // Has incoming arg of type CODEPTR
 	bool HasInArgDataPointer; // Has incoming arg of type POINTER or a refinement of POINTER
 	bool HasMallocCall; // calls malloc()
@@ -827,6 +849,7 @@ private:
 	std::vector<int> LoopHeadBlockNumbers; // indexed by loop number; block number of header block
 	std::vector<std::set<int> > LoopExitTargets; // indexed by loop number; block number of exit destinations
 	std::vector<std::map<int, STARSBitSet> > LoopExitTargetsReachabilitySets; // 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<std::vector<struct LoopExitingBlockInfo> > LoopExitingBlocksVector; // indexed by LoopNum, info about each block that can exit the loop
 	std::vector<bool> LoopHasMultipleExits; 
 	std::vector<bool> LoopWritesMemory; // static, indirect or indexed writes
 	std::vector<bool> LoopReadsMemory; // static, indirect or indexed reads
@@ -1134,7 +1157,6 @@ private:
 	bool PropagateSignedness(void); // Propagate signedness FG info from DEFs to USEs whenever there is no USE sign info.
 	bool FindLoopContinuePattern(const int BranchBlockNum); // Does code starting at COND_BRANCH in BranchBlockNum represent a C/C++ loop continue statement?
 	bool LoopContinueHelper(const int BranchBlockNum, const int InnerMostLoopNum, const SMPBasicBlock *CurrentBlock);
-	void MarkSpecialNumericErrorCases(void); // Detect and mark special cases before emitting numeric error annotations.
 	void MarkLoopContinueCases(const SMPBasicBlock *CurrBlock, const int HeaderBlockNum, const std::size_t BlockIndex, const STARS_ea_t InstAddr); // refactored helper for MarkSpecialNumericErrorCases()
 	void EmitReturnTargetAnnotations(void); // Emit Indirect Branch Target destinations for return instructions in this func.
 	void EmitFuncPtrShadowingAnnotations(FILE *InfoAnnotFile); // Emit annotations for func ptr shadowing defense
diff --git a/include/interfaces/SMPDBInterface.h b/include/interfaces/SMPDBInterface.h
index a48f393cd61642fc29b37abb3017e909940bec0e..e75fd123270ad782f126474c6d6065aafdf70280 100644
--- a/include/interfaces/SMPDBInterface.h
+++ b/include/interfaces/SMPDBInterface.h
@@ -93,6 +93,7 @@
 #define STARS_PSEUDO_ID_MIN  ((STARS_ea_t) STARS_BADADDR - STARS_BLOCKNUM_MASK)
 #define STARS_PSEUDO_BLOCKNUM_MAX ((STARS_ea_t) STARS_BADADDR - 3)
 
+#define STARS_IsNotPseudoInstID(addr) (STARS_PSEUDO_ID_MIN > addr)
 #define STARS_IsLiveInPseudoID(addr) (STARS_LIVEIN_PSEUDO_ID == ((STARS_ea_t) addr))
 #define STARS_IsSSAMarkerPseudoID(addr) (STARS_SSA_MARKER_PSEUDO_ID == ((STARS_ea_t) addr))
 #define STARS_IsBlockNumPseudoID(addr) ((STARS_PSEUDO_ID_MIN <= ((STARS_ea_t) addr)) && (STARS_PSEUDO_BLOCKNUM_MAX >= ((STARS_ea_t) addr)))
diff --git a/src/base/SMPBasicBlock.cpp b/src/base/SMPBasicBlock.cpp
index 4093f8b6decb04ee867675c7dfd6187ef43a465a..e750d7571b6b6505c9de95e3fe013938f05b1ae0 100644
--- a/src/base/SMPBasicBlock.cpp
+++ b/src/base/SMPBasicBlock.cpp
@@ -1732,8 +1732,10 @@ SMPInstr * SMPBasicBlock::FindBranchCompareOrTest(SMPoperator &BranchOperator, S
 	bool EndsWithCondBranch = ((COND_BRANCH == BranchInst->GetDataFlowType()) && (!EndsWithLoopInst));
 
 	// NOTE: Handle loop opcodes later.
-	if (EndsWithLoopInst)
+	if (EndsWithLoopInst) {
+		DecAddr = STARS_BADADDR;
 		return CompareOrTestInst;
+	}
 
 	if (!SearchCase) {
 		BranchOperator = BranchInst->GetCondBranchOperator();
@@ -1779,6 +1781,7 @@ SMPInstr * SMPBasicBlock::FindBranchCompareOrTest(SMPoperator &BranchOperator, S
 					// Something besides compare, test or decrement set the flags.
 					SMP_msg("ERROR: COND_BRANCH: Flags set by unexpected opcode in inst at %llx: CurrSSA: %d \n",
 						(uint64_t) InstAddr, CurrFlagsSSANum);
+					CurrInst->Dump();
 				}
 				else {
 					SMP_msg("ERROR: COND_BRANCH: Flags SSANum did not match in block at %llx: CurrSSA: %d SearchSSA: %d\n",
diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp
index 80b703e2371bf39e87b544797f5566858bb0fc05..c5c68baa6ce332356f3b5ccc9580ceb2607b1ac7 100644
--- a/src/base/SMPFunction.cpp
+++ b/src/base/SMPFunction.cpp
@@ -300,6 +300,7 @@ SMPFunction::SMPFunction(STARS_Function_t *Info, SMPProgram* pgm) {
 	this->StackFrameExtendsPastStackTop = false;
 	this->SetIsSpeculative(false);
 	this->HasHashingCode = false;
+	this->HasShortCircuitExpr = false;
 	this->HasInArgCodePointer = false;
 	this->HasInArgDataPointer = false;
 	this->HasMallocCall = false;
@@ -1356,6 +1357,11 @@ void SMPFunction::IncrementJumpToFollowNodeCounter(STARS_ea_t InstAddr) {
 	return;
 }
 
+void SMPFunction::SetHasUnstructuredCFG(void) { 
+	this->HasStructuredCFG = false;
+	return;
+} // end of SMPFunction::SetHasUnstructuredCFG()
+
 // Add a caller to the list of all callers of this function.
 void SMPFunction::AddCallSource(STARS_ea_t addr) {
 	// Convert call instruction address to beginning address of the caller.
@@ -7111,12 +7117,11 @@ void SMPFunction::FindLoopBlocksFromTailToHeader(const size_t LoopNumber, const
 
 // Detect which blocks are in which loops and populate FuncLoopsByBlock and FuncBlocksByLoop data structures.
 void SMPFunction::DetectLoops(void) {
-	list<SMPBasicBlock *>::iterator BlockIter;
 	map<int, int> DoubleTailBlockNumToFollowBlockMap; // keep track of tricky FollowBlockNum
 		// analysis results for DoubleTailBlocks
 
 	std::size_t LoopNumber = 0;
-	for (BlockIter = this->Blocks.begin(); BlockIter != this->Blocks.end(); ++BlockIter) {
+	for (list<SMPBasicBlock *>::iterator BlockIter = this->Blocks.begin(); BlockIter != this->Blocks.end(); ++BlockIter) {
 		SMPBasicBlock *CurrBlock = (*BlockIter);
 		if (CurrBlock->IsLoopTailBlock()) {
 			// For each loop tail block, get its loop header block number (the target
@@ -7216,6 +7221,16 @@ void SMPFunction::DetectLoops(void) {
 			}
 
 			this->ClassifyLoop(LoopNumber, HeaderExitFollowNum, TailExitFollowNum, CurrBlock, HeadBlock, HeaderBlockExitsLoop, TailBlockExitsLoop);
+			if (this->LoopExitingBlocksVector.size() <= LoopNumber) {
+				// Loop must have had no exits.
+				assert(STARS_INFINITE_OR_MIDDLE_TESTING_LOOP == this->LoopTypesByLoopNum[LoopNumber]);
+				SMP_msg("INFO: LOOP: Infinite loop, no exiting blocks, loop number %zu ", LoopNumber);
+				this->DumpFuncNameAndAddr();
+				vector<struct LoopExitingBlockInfo> NewVector;
+				this->LoopExitingBlocksVector.push_back(NewVector);
+				assert(this->LoopExitingBlocksVector.size() > LoopNumber);
+			}
+
 			if (DoubleTailFlag) {
 				// Classify the outer loop.
 				HeadBlockNum = CurrBlock->GetOuterLoopHeaderNumberForDoubleTailBlock();
@@ -7324,14 +7339,64 @@ void SMPFunction::DetectLoopFollowBlock(const size_t LoopNumber) {
 
 	for (size_t BlockNum : LoopBlockNums) {
 		SMPBasicBlock *CurrBlock = this->GetBlockByNum(BlockNum);
-		for (list<SMPBasicBlock *>::const_iterator SuccIter = CurrBlock->GetFirstConstSucc(); SuccIter != CurrBlock->GetLastConstSucc(); ++SuccIter) {
-			int SuccBlockNum = (*SuccIter)->GetNumber();
+		for (SMPBasicBlock *SuccBlock : CurrBlock->GetConstSuccList()) {
+			int SuccBlockNum = SuccBlock->GetNumber();
 			assert(LoopNumber < this->FuncBlocksByLoop.size());
 			assert(SuccBlockNum >= 0);
 			assert(((size_t) SuccBlockNum) < this->GetNumBlocks());
 			assert(((size_t)SuccBlockNum) < this->FuncBlocksByLoop[LoopNumber].GetNumBits());
 			if (!this->FuncBlocksByLoop[LoopNumber].GetBit((size_t) SuccBlockNum)) {
 				// Successor is not in loop.
+
+				// Record exiting block info.
+				struct LoopExitingBlockInfo CurrExitInfo;
+				CurrExitInfo.ExitingBlockNum = (int)BlockNum;
+				CurrExitInfo.TargetBlockNum = SuccBlockNum;
+				CurrExitInfo.CompareTestDecInst = nullptr;
+				CurrExitInfo.ShortCircuitExpr = false;
+				CurrExitInfo.ReferencesBIV = false;
+
+				// Can we trace the conditional branch of the tail and/or header blocks
+				//  to a compare, test, decrement or other inst that can be cleanly analyzed for
+				//  our loop iterations count expression?
+				SMPInstr *CompareOrTestInst = nullptr;
+				SMPInstr *DecInst = nullptr;
+				STARS_ea_t DecAddr = STARS_BADADDR;
+				if (CurrBlock->HasConditionalBranch()) {
+					SMPoperator BranchOper;
+					CompareOrTestInst = CurrBlock->FindBranchCompareOrTest(BranchOper, DecAddr, false, SMP_SSA_UNINIT);
+					if (STARS_BADADDR != DecAddr) {
+						assert(STARS_IsNotPseudoInstID(DecAddr));
+						DecInst = this->GetInstFromAddr(DecAddr);
+						assert(nullptr != DecInst);
+						CurrExitInfo.CompareTestDecInst = DecInst;
+					}
+					else if (nullptr != CompareOrTestInst) {
+						CurrExitInfo.CompareTestDecInst = CompareOrTestInst;
+					}
+				}
+				// Record whether branch is a short circuit expr branch.
+				// Due to phase ordering, this has not been determined until SPARK analysis in 
+				//  MarkSpecialNumericErrorCases(), so it must be filled in later.
+				CurrExitInfo.ShortCircuitExpr = false;
+
+				// If first exiting block, expand outer vector, else push onto inner vector.
+				if (LoopNumber < this->LoopExitingBlocksVector.size()) {
+					this->LoopExitingBlocksVector[LoopNumber].push_back(CurrExitInfo);
+				}
+				else {
+					// Must have had an infinite loop, or we are processing loops out of order.
+					while (this->LoopExitingBlocksVector.size() < LoopNumber) {
+						// Pad out with empty vectors.
+						vector<struct LoopExitingBlockInfo> NewVector;
+						this->LoopExitingBlocksVector.push_back(NewVector);
+					}
+					vector<struct LoopExitingBlockInfo> NewVector;
+					NewVector.push_back(CurrExitInfo);
+					this->LoopExitingBlocksVector.push_back(NewVector);
+				}
+
+				// Record loop follow block info.
 				this->UpdateLoopFollowBlockNum(HeadBlockNum, SuccBlockNum);
 			}
 		}
@@ -7340,12 +7405,11 @@ void SMPFunction::DetectLoopFollowBlock(const size_t LoopNumber) {
 	return;
 } // end of SMPFunction::DetectLoopFollowBlock()
 
-void
-SMPFunction::ClassifyLoop(size_t LoopNumber, int HeaderExitFollowNum, int TailExitFollowNum, SMPBasicBlock *CurrBlock, SMPBasicBlock *HeadBlock, bool HeaderBlockExitsLoop, bool TailBlockExitsLoop) {
+void SMPFunction::ClassifyLoop(size_t LoopNumber, int HeaderExitFollowNum, int TailExitFollowNum, SMPBasicBlock *CurrBlock, SMPBasicBlock *HeadBlock, bool HeaderBlockExitsLoop, bool TailBlockExitsLoop) {
 	bool VerboseOutput = global_stars_interface->VerboseSPARKMode();
 	this->DetectLoopFollowBlock(LoopNumber);
 	if (HeaderBlockExitsLoop && HeadBlock->HasIndirectJump()) {
-		this->HasStructuredCFG = false; // indirect jump head loop exit
+		this->SetHasUnstructuredCFG(); // indirect jump head loop exit
 		if (!this->PrintedSPARKUnstructuredMsg) {
 			SMP_msg("ERROR: SPARK: Unstructured due to indirect jump head loop exit at %llx for loop %d ",
 				(uint64_t)CurrBlock->GetLastAddr(), LoopNumber);
@@ -7354,7 +7418,7 @@ SMPFunction::ClassifyLoop(size_t LoopNumber, int HeaderExitFollowNum, int TailEx
 		}
 	}
 	else if (TailBlockExitsLoop && CurrBlock->HasIndirectJump()) {
-		this->HasStructuredCFG = false; // indirect jump tail loop exit 
+		this->SetHasUnstructuredCFG(); // indirect jump tail loop exit 
 		if (!this->PrintedSPARKUnstructuredMsg) {
 			SMP_msg("ERROR: SPARK: Unstructured due to indirect jump tail loop exit at %llx for loop %d ",
 				(uint64_t)CurrBlock->GetLastAddr(), LoopNumber);
@@ -7366,7 +7430,7 @@ SMPFunction::ClassifyLoop(size_t LoopNumber, int HeaderExitFollowNum, int TailEx
 	if (TailBlockExitsLoop) {
 		if (HeaderBlockExitsLoop) {
 			// Conditional exits at top and bottom of loop.
-			this->LoopTypesByLoopNum[LoopNumber] = STARS_BOTTOM_TESTING_LOOP;
+			this->LoopTypesByLoopNum[LoopNumber] = STARS_TOP_AND_BOTTOM_TESTING_LOOP;
 			if (TailExitFollowNum != HeaderExitFollowNum) {
 				if (this->HasGoodLoopFollowBlocks || VerboseOutput) {
 					if (!this->PrintedSPARKUnstructuredMsg || VerboseOutput) {
@@ -7401,6 +7465,45 @@ SMPFunction::ClassifyLoop(size_t LoopNumber, int HeaderExitFollowNum, int TailEx
 			this->LoopTestBlocksByLoopNum[LoopNumber] = SMP_BLOCKNUM_UNINIT;
 		}
 	}
+
+#if 1
+	// See if we want to reclassify the loop according to which COND_BRANCH controls maximum iterations.
+	//  A loop could have an induction var that controls iteration count, but also have a possible early
+	//  exit based on some condition. The early exit does not control maximum iterations. Often the early
+	//  exit is not a simple induction var test, so it fails to match up with a compare or test inst.
+
+	// Select the most analyzeable test block when we have more than one exiting block.
+
+	// First, pad out the vector allocation if needed.
+	while (this->LoopExitingBlocksVector.size() <= LoopNumber) {
+		// Loop must have had no exits.
+		assert(STARS_INFINITE_OR_MIDDLE_TESTING_LOOP == this->LoopTypesByLoopNum[LoopNumber]);
+		SMP_msg("INFO: LOOP: Infinite loop, no exiting blocks, loop number %zu ", LoopNumber);
+		this->DumpFuncNameAndAddr();
+
+		vector<struct LoopExitingBlockInfo> NewVector;
+		this->LoopExitingBlocksVector.push_back(NewVector);
+	}
+
+	if (1 < this->LoopExitingBlocksVector[LoopNumber].size()) {
+		for (size_t VecIndex = 0; VecIndex < this->LoopExitingBlocksVector[LoopNumber].size(); ++VecIndex) {
+			if (nullptr != this->LoopExitingBlocksVector[LoopNumber][VecIndex].CompareTestDecInst) {
+				int GoodExitBlockNum = this->LoopExitingBlocksVector[LoopNumber][VecIndex].ExitingBlockNum;
+				if (GoodExitBlockNum != this->LoopTestBlocksByLoopNum[LoopNumber]) {
+					SMP_msg("INFO: LOOP: Changing loop test block from %d to traceable block %d for loop %zu type %d ",
+						this->LoopTestBlocksByLoopNum[LoopNumber], GoodExitBlockNum, LoopNumber, this->LoopTypesByLoopNum[LoopNumber]);
+					this->DumpFuncNameAndAddr();
+					this->LoopTestBlocksByLoopNum[LoopNumber] = GoodExitBlockNum;
+				}
+			}
+			else if (VerboseOutput) {
+				SMP_msg("INFO: LOOP: Skipping untraceable loop test block %d for loop %zu ",
+					this->LoopTestBlocksByLoopNum[LoopNumber], LoopNumber);
+			}
+		}
+	}
+#endif
+
 	return;
 } // end of SMPFunction::ClassifyLoop()
 
@@ -7423,7 +7526,7 @@ bool SMPFunction::DoesBlockExitLoop(std::size_t LoopNumber, SMPBasicBlock *LoopB
 						this->DumpFuncNameAndAddr();
 						this->PrintedSPARKUnstructuredMsg = true;
 					}
-					this->HasStructuredCFG = false; // multi-level loop break
+					this->SetHasUnstructuredCFG(); // multi-level loop break
 				}
 				break;
 			}
@@ -7499,7 +7602,7 @@ void SMPFunction::ComputeLoopFollowNodesReachability(const std::size_t LoopNum)
 				this->DumpFuncNameAndAddr();
 				this->PrintedSPARKUnstructuredMsg = true;
 			}
-			this->HasStructuredCFG = false;
+			this->SetHasUnstructuredCFG();
 			break;
 		}
 	}
@@ -7538,7 +7641,7 @@ void SMPFunction::ComputeLoopFollowNodesReachability(const std::size_t LoopNum)
 				this->DumpFuncNameAndAddr();
 				this->PrintedSPARKUnstructuredMsg = true;
 			}
-			this->HasStructuredCFG = false; // multi-exit loop has no single convergence point of follow nodes.
+			this->SetHasUnstructuredCFG(); // multi-exit loop has no single convergence point of follow nodes.
 			// TODO: If the multiple termination blocks all loop back to the same outer loop head block, this
 			//  is structured code and can be translated. !!!!****!!!!
 		}
@@ -7567,7 +7670,7 @@ void SMPFunction::ComputeLoopFollowNodesReachability(const std::size_t LoopNum)
 									this->DumpFuncNameAndAddr();
 									this->PrintedSPARKUnstructuredMsg = true;
 								}
-								this->HasStructuredCFG = false; // multi-exit loop has a need to pass boolean vars as args, alter translation of outer loop
+								this->SetHasUnstructuredCFG(); // multi-exit loop has a need to pass boolean vars as args, alter translation of outer loop
 								break; // stop after first problem found
 							}
 						}
@@ -8786,8 +8889,8 @@ void SMPFunction::DetectLoopInductionVars2(void) {
 	list<size_t> BlockList;
 	for (size_t LoopIndex = 0; LoopIndex < this->LoopHeadBlockNumbers.size(); ++LoopIndex) {
 		this->BuildLoopBlockList(LoopIndex, BlockList);
-		for (list<size_t>::const_iterator BlockIter = BlockList.cbegin(); BlockIter != BlockList.cend(); ++BlockIter) {
-			SMPBasicBlock *CurrBlock = this->GetBlockByNum(*BlockIter);
+		for (size_t BlockIndex : BlockList) {
+			SMPBasicBlock *CurrBlock = this->GetBlockByNum(BlockIndex);
 			for (vector<SMPInstr *>::iterator InstIter = CurrBlock->GetFirstInst(); InstIter != CurrBlock->GetLastInst(); ++InstIter) {
 				SMPInstr *CurrInst = (*InstIter);
 				STARSOpndTypePtr Mult1 = nullptr, Mult2 = nullptr, Add1 = nullptr, Add2 = nullptr;
@@ -8856,6 +8959,7 @@ bool SMPFunction::IsLoopInductionVar(std::size_t LoopIndex, STARSOpndTypePtr &Cu
 //  Do not modify ListIter or FamilyIndex if we are returning false.
 // Same as IsLoopInductionVar() without requiring any SSA nums to match, i.e. is CurrOp an IV.
 bool SMPFunction::IsLoopInductionVarForAnySSANum(std::size_t LoopIndex, const STARSOpndTypePtr &CurrOp, STARSInductionVarFamilyList::iterator &ListIter, std::size_t &FamilyIndex) {
+	assert(this->LoopInductionVars.size() > LoopIndex);
 	STARSInductionVarFamilyList::iterator TempIter;
 
 	for (TempIter = this->LoopInductionVars[LoopIndex].begin(); TempIter != this->LoopInductionVars[LoopIndex].end(); ++TempIter) {
@@ -9661,7 +9765,7 @@ STARSExpression* SMPFunction::CreateIterationsExpr(std::size_t LoopIndex, const
 
 	STARS_uval_t IncDecValue = IVFamily.BasicInductionVar.Addend.GetOp()->GetImmedValue();
 	// bool PositiveIncrement = (!IVFamily.BasicInductionVar.SubtractAddend);
-	bool BottomTestingLoop = (this->LoopTypesByLoopNum[LoopIndex] == STARS_BOTTOM_TESTING_LOOP);
+	bool BottomTestingLoop = DoesLoopTestAtBottom(this->LoopTypesByLoopNum[LoopIndex]);
 
 	// For loops with a BIV that counts upward by 1:
 	//
@@ -11601,7 +11705,7 @@ void SMPFunction::FindSwitchIDom(struct SwitchTableInfo &TableInfo) {
 						this->DumpFuncNameAndAddr();
 						this->PrintedSPARKUnstructuredMsg = true;
 					}
-					this->HasStructuredCFG = false; // Bad switch control flow
+					this->SetHasUnstructuredCFG(); // Bad switch control flow
 				}
 			}
 			else if ((INDIR_JUMP == FlowType) && (PredBlock->GetNumber() == TableInfo.IndirJumpBlockNum)) {
@@ -11718,6 +11822,7 @@ void SMPFunction::CoalesceShadowBlocks(int LeftTCFGBlockNum, int RightTCFGBlockN
 		this->SetControlFlowType(RightLastAddr, SHORT_CIRCUIT_BRANCH);
 	}
 
+	this->HasShortCircuitExpr = true;
 	return;
 } // end of SMPFunction::CoalesceShadowBlocks()
 
@@ -12484,7 +12589,7 @@ bool SMPFunction::AnalyzeConditionalStatements(void) {
 									this->DumpFuncNameAndAddr();
 									this->PrintedSPARKUnstructuredMsg = true;
 								}
-								this->HasStructuredCFG = false; // DistantBlock != FollowBlock for normal if-then
+								this->SetHasUnstructuredCFG(); // DistantBlock != FollowBlock for normal if-then
 							}
 						}
 						else if (DistantBlockNum == FollowNodeNum) {
@@ -12494,7 +12599,7 @@ bool SMPFunction::AnalyzeConditionalStatements(void) {
 								this->DumpFuncNameAndAddr();
 								this->PrintedSPARKUnstructuredMsg = true;
 							}
-							this->HasStructuredCFG = false; // DistantBlock == FollowBlock for OddIfThenCase
+							this->SetHasUnstructuredCFG(); // DistantBlock == FollowBlock for OddIfThenCase
 						}
 					}
 					else {
@@ -12922,7 +13027,7 @@ int SMPFunction::FindConditionalFollowNode2(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;  // Inconsistent loop head block nums; irrecoverable problem
+								this->SetHasUnstructuredCFG();  // Inconsistent loop head block nums; irrecoverable problem
 								return SMP_BLOCKNUM_UNINIT;
 #else
 								LoopBackCounter = 0;
@@ -14234,7 +14339,7 @@ void SMPFunction::MarkBlocksAndClone(const int StartingBlockNum, const int Unlin
 				// Case 2.
 #if 0
 				if (UnlinkBlockNum != SourceTCFGBlockNum) {
-					this->HasStructuredCFG = false;
+					this->SetHasUnstructuredCFG();
 					SMP_msg("ERROR: SPARK: Cannot update jump table entry %d to %d with UnlinkBlockNum %d ",
 						SourceTCFGBlockNum, TargetTCFGBlockNum, UnlinkBlockNum);
 					this->DumpFuncNameAndAddr();
@@ -14841,7 +14946,7 @@ int SMPFunction::TrackConditionalBranchTerminus(int BranchHeadBlockNum, int Curr
 				this->DumpFuncNameAndAddr();
 				TerminusBlockNum = SMP_BLOCKNUM_UNINIT; // error signal
 				WorkListBlockNums.clear();
-				this->HasStructuredCFG = false; // recovery of blocks into if-elsif-elsif-else is not possible
+				this->SetHasUnstructuredCFG(); // recovery of blocks into if-elsif-elsif-else is not possible
 				break;
 			}
 			else if (STARS_COND_BRANCH_WORKLIST_LIMIT < WorkListBlockNums.size()) {
@@ -14850,7 +14955,7 @@ int SMPFunction::TrackConditionalBranchTerminus(int BranchHeadBlockNum, int Curr
 				this->DumpFuncNameAndAddr();
 				TerminusBlockNum = SMP_BLOCKNUM_UNINIT; // error signal
 				WorkListBlockNums.clear();
-				this->HasStructuredCFG = false; // recovery of blocks into if-elsif-elsif-else is not possible
+				this->SetHasUnstructuredCFG(); // recovery of blocks into if-elsif-elsif-else is not possible
 				break;
 			}
 			else if (STARS_COND_BRANCH_ALREADY_SEEN_LIMIT < BlockAlreadySeenCounter) {
@@ -14859,7 +14964,7 @@ int SMPFunction::TrackConditionalBranchTerminus(int BranchHeadBlockNum, int Curr
 				this->DumpFuncNameAndAddr();
 				TerminusBlockNum = SMP_BLOCKNUM_UNINIT; // error signal
 				WorkListBlockNums.clear();
-				this->HasStructuredCFG = false; // recovery of blocks into if-elsif-elsif-else is not possible
+				this->SetHasUnstructuredCFG(); // recovery of blocks into if-elsif-elsif-else is not possible
 				break;
 			}
 
@@ -17709,78 +17814,8 @@ void SMPFunction::BuildBlockListFromBitset(const STARSBitSet &CurrBitSet, list<s
 	return;
 } // end of SMPFunction::BuildBlockListFromBitset()
 
-// Analyze how many times each loop iterates
-void SMPFunction::AnalyzeLoopIterations(void) {
-	bool VerboseOutput = global_stars_interface->VerboseLoopsMode();
-	bool DebugFlag = false;
-	DebugFlag = (0x417710 == this->GetFirstFuncAddr());
-	// DebugFlag = (0x402730 == this->GetFirstFuncAddr());
-	VerboseOutput = (VerboseOutput || DebugFlag);
-	FILE *InfoAnnotFile = global_STARS_program->GetInfoAnnotFile();
-	if (0 < this->GetNumLoops()) {
-		// Get ready to mark memory writes by loop.
-		STARSBitSet TempPositiveBitSet;
-		TempPositiveBitSet.AllocateBits(this->MaxStackAccessLimit);
-		STARSBitSet TempNegativeBitSet;
-		TempNegativeBitSet.AllocateBits(0 - this->MinStackAccessOffset);
-		for (unsigned i = 0; i < this->LoopCount; ++i) {
-			this->NegativeOffsetStackBytesWrittenByLoop.push_back(TempNegativeBitSet);
-			this->PositiveOffsetStackBytesWrittenByLoop.push_back(TempPositiveBitSet);
-		}
-	}
-
-	this->LoopIterationsInitExprs.resize(this->LoopCount, nullptr);
-	this->LoopIterationsLimitExprs.resize(this->LoopCount, nullptr);
-	this->LoopIterationsCountExprs.resize(this->LoopCount, nullptr);
-	this->LoopMemWriteRangeExprs.resize(this->LoopCount);
-	this->LoopMemWriteBoundsExprs.resize(this->LoopCount);
-	this->LoopMemWriteBoundsExprsExpanded.resize(this->LoopCount);
-	this->StringMemWriteRangeExprs.resize(this->LoopCount + 1);
-	this->StringMemWriteRangeWidths.resize(this->LoopCount + 1);
-	this->LoopRegHashSets.resize(this->LoopCount);
-	this->LoopRegSourceExprPairs.resize(this->LoopCount);
-	this->LoopIVUsedAsStringWriteCounter.resize(this->LoopCount);
-	this->NonStackFrameLoopMemWrites.resize(this->LoopCount, false);
-	this->LoopMemRangeInArgRegsBitmap.resize(this->LoopCount);
-	this->OutputRegsByLoop.resize(this->LoopCount);
-	this->CalleePreservedRegsByLoop.resize(this->LoopCount);
+void SMPFunction::BuildLoopIterationCountExprs(const bool VerboseOutput, FILE *InfoAnnotFile) {
 	std::bitset<1 + MD_LAST_REG_NO> TempBitset(0);
-	this->MemRangeRegsBitmap = TempBitset;
-	this->LoopAnalyzedBIVIters.resize(this->LoopCount);
-	this->LoopWritesGlobalStaticMemory.resize(this->LoopCount, false);
-	this->LoopReadsGlobalStaticMemory.resize(this->LoopCount, false);
-	this->LoopHasCalleeMemWrites.resize(this->LoopCount, false);
-	this->LoopUsesStackPtrRegs.resize(this->LoopCount, true); // default to the most common case
-	this->LoopHasPreconditions.resize(this->LoopCount, true); // default to the most common case
-	this->LoopExecutesWithLimitValue.resize(this->LoopCount, false);
-	this->LoopAnalysisProblems.resize(this->LoopCount, false);
-	this->CalleeMemExprProblems.resize(this->LoopCount + 1, false);
-	this->SymbolicAnalysisProblems.resize(this->LoopCount + 1, false);
-	this->LoopIncrementValue.resize(this->LoopCount, 0); // default to invalid case
-	this->LoopMemAddrExprsFromCallees.resize(this->LoopCount);
-	this->LoopMemAddrExprWidthsFromCallees.resize(this->LoopCount);
-	this->LoopMemExprsExpandToStackOffsets.resize(this->LoopCount, false);
-	this->LoopMemAddrExprWidthsFromCalleeLoops.resize(this->LoopCount + 1);
-	this->LoopMemAddrExprsFromCalleeLoops.resize(this->LoopCount + 1);
-	this->MemAddrExprsFromCallees.resize(this->LoopCount + 1);
-	this->MemAddrExprWidthsFromCallees.resize(this->LoopCount + 1);
-	this->NonStackFrameCalleeMemWrites.resize(this->LoopCount + 1);
-	this->InArgsUsedInMemWrites.resize(this->LoopCount + 1);
-	this->InArgsUsedInMemWriteByteWidths.resize(this->LoopCount + 1);
-	this->StoppedOnIVMemRangeExprs.resize(this->LoopCount + 1);
-	this->StoppedOnIVNonRangeExprs.resize(this->LoopCount + 1);
-	this->StoppedOnIVMemRangeIterWidths.resize(this->LoopCount + 1);
-	this->StoppedOnIVNonRangeIterWidths.resize(this->LoopCount + 1);
-	this->RelationalLowerBoundExprs.resize(this->LoopCount + 1);
-	this->RelationalUpperBoundExprs.resize(this->LoopCount + 1);
-	this->RelationalMemWriteWidths.resize(this->LoopCount + 1);
-
-	if (!this->HasStructuredControlFlow())
-		return; // just allocate data structures above to avoid crashes, then exit.
-
-	// Prepare for limited interprocedural constant propagation
-	//  by finding constant InArg values.
-	this->ComputeInArgConstValues();
 
 	for (size_t LoopIndex = 0; LoopIndex < this->LoopCount; ++LoopIndex) {
 		this->LoopMemRangeInArgRegsBitmap[LoopIndex] = TempBitset;
@@ -17793,10 +17828,10 @@ void SMPFunction::AnalyzeLoopIterations(void) {
 		int TestBlockNum = this->LoopTestBlocksByLoopNum[LoopIndex];
 		int LoopType = this->LoopTypesByLoopNum[LoopIndex];
 		bool LowerLimit = false, UpperLimit = false; // Loop terminates by becoming greater than UpperLimit, or less than LowerLimit?
-		STARSDefUseIter ExitUse1, ExitUse2; // iterators for the 
+		STARSDefUseIter ExitUse1, ExitUse2; // iterators for the UseOps involved in conditional loop exit
 		STARS_uval_t ExitConstUse2 = 0; // const value for exit comparison instead of ExitUse2
 		bool CompareAgainstConst = false; // compare ExitUse1 against ExitConstUse2 if true, else ExitUse1 vs. ExitUse2
-		if ((SMP_BLOCKNUM_UNINIT != TestBlockNum) && ((LoopType == STARS_TOP_TESTING_LOOP) || (LoopType == STARS_BOTTOM_TESTING_LOOP))) {
+		if ((SMP_BLOCKNUM_UNINIT != TestBlockNum) && (DoesLoopTestAtTop(LoopType) || DoesLoopTestAtBottom(LoopType))) {
 			SMPBasicBlock *TestBlock = this->GetBlockByNum(TestBlockNum);
 			int FollowBlockNum = SMP_BLOCKNUM_UNINIT;
 			bool MultiExitLoop = this->GetLoopFollowBlockNum(LoopIndex, FollowBlockNum);
@@ -17837,7 +17872,7 @@ void SMPFunction::AnalyzeLoopIterations(void) {
 				}
 				else {
 					SMP_msg("ERROR: LOOP: Decrement with BranchOperator %d in test block %d DecrementAddr %llx loop %u ",
-						BranchOperator, TestBlockNum, (uint64_t) DecrementAddr, LoopIndex);
+						BranchOperator, TestBlockNum, (uint64_t)DecrementAddr, LoopIndex);
 					this->DumpFuncNameAndAddr();
 					this->LoopComparisonExprs.push_back(CurrentLoopComparisonExpr);
 					this->LoopAnalysisProblems[LoopIndex] = true;
@@ -17866,7 +17901,7 @@ void SMPFunction::AnalyzeLoopIterations(void) {
 			this->DumpFuncNameAndAddr();
 			for (STARSInductionVarFamilyIter IVarVecIter = this->LoopInductionVars[LoopIndex].begin();
 				IVarVecIter != this->LoopInductionVars[LoopIndex].end();
-			++IVarVecIter) {
+				++IVarVecIter) {
 
 				int OutsideDefSSANum = (*IVarVecIter).BIVIncomingSSANum;
 				if (OutsideDefSSANum != SMP_SSA_UNINIT) {
@@ -18075,7 +18110,85 @@ void SMPFunction::AnalyzeLoopIterations(void) {
 				}
 			} // end for all IV iters in current LoopIndex
 		}
-	} // end for LoopIndex: loop 1, iteration count analysis
+	} // end for all LoopIndex values
+
+	return;
+} // end of SMPFunction::BuildLoopIterationCountExprs()
+
+// Analyze how many times each loop iterates
+void SMPFunction::AnalyzeLoopIterations(void) {
+	bool DebugFlag = false;
+	DebugFlag = (0x804f596 == this->GetFirstFuncAddr());
+	// DebugFlag = (0x402730 == this->GetFirstFuncAddr());
+	bool VerboseOutput = DebugFlag || global_stars_interface->VerboseLoopsMode();
+	FILE *InfoAnnotFile = global_STARS_program->GetInfoAnnotFile();
+	if (0 < this->GetNumLoops()) {
+		// Get ready to mark memory writes by loop.
+		STARSBitSet TempPositiveBitSet;
+		TempPositiveBitSet.AllocateBits(this->MaxStackAccessLimit);
+		STARSBitSet TempNegativeBitSet;
+		TempNegativeBitSet.AllocateBits(0 - this->MinStackAccessOffset);
+		for (unsigned i = 0; i < this->LoopCount; ++i) {
+			this->NegativeOffsetStackBytesWrittenByLoop.push_back(TempNegativeBitSet);
+			this->PositiveOffsetStackBytesWrittenByLoop.push_back(TempPositiveBitSet);
+		}
+	}
+
+	this->LoopIterationsInitExprs.resize(this->LoopCount, nullptr);
+	this->LoopIterationsLimitExprs.resize(this->LoopCount, nullptr);
+	this->LoopIterationsCountExprs.resize(this->LoopCount, nullptr);
+	this->LoopMemWriteRangeExprs.resize(this->LoopCount);
+	this->LoopMemWriteBoundsExprs.resize(this->LoopCount);
+	this->LoopMemWriteBoundsExprsExpanded.resize(this->LoopCount);
+	this->StringMemWriteRangeExprs.resize(this->LoopCount + 1);
+	this->StringMemWriteRangeWidths.resize(this->LoopCount + 1);
+	this->LoopRegHashSets.resize(this->LoopCount);
+	this->LoopRegSourceExprPairs.resize(this->LoopCount);
+	this->LoopIVUsedAsStringWriteCounter.resize(this->LoopCount);
+	this->NonStackFrameLoopMemWrites.resize(this->LoopCount, false);
+	this->LoopMemRangeInArgRegsBitmap.resize(this->LoopCount);
+	this->OutputRegsByLoop.resize(this->LoopCount);
+	this->CalleePreservedRegsByLoop.resize(this->LoopCount);
+	std::bitset<1 + MD_LAST_REG_NO> TempBitset(0);
+	this->MemRangeRegsBitmap = TempBitset;
+	this->LoopAnalyzedBIVIters.resize(this->LoopCount);
+	this->LoopWritesGlobalStaticMemory.resize(this->LoopCount, false);
+	this->LoopReadsGlobalStaticMemory.resize(this->LoopCount, false);
+	this->LoopHasCalleeMemWrites.resize(this->LoopCount, false);
+	this->LoopUsesStackPtrRegs.resize(this->LoopCount, true); // default to the most common case
+	this->LoopHasPreconditions.resize(this->LoopCount, true); // default to the most common case
+	this->LoopExecutesWithLimitValue.resize(this->LoopCount, false);
+	this->LoopAnalysisProblems.resize(this->LoopCount, false);
+	this->CalleeMemExprProblems.resize(this->LoopCount + 1, false);
+	this->SymbolicAnalysisProblems.resize(this->LoopCount + 1, false);
+	this->LoopIncrementValue.resize(this->LoopCount, 0); // default to invalid case
+	this->LoopMemAddrExprsFromCallees.resize(this->LoopCount);
+	this->LoopMemAddrExprWidthsFromCallees.resize(this->LoopCount);
+	this->LoopMemExprsExpandToStackOffsets.resize(this->LoopCount, false);
+	this->LoopMemAddrExprWidthsFromCalleeLoops.resize(this->LoopCount + 1);
+	this->LoopMemAddrExprsFromCalleeLoops.resize(this->LoopCount + 1);
+	this->MemAddrExprsFromCallees.resize(this->LoopCount + 1);
+	this->MemAddrExprWidthsFromCallees.resize(this->LoopCount + 1);
+	this->NonStackFrameCalleeMemWrites.resize(this->LoopCount + 1);
+	this->InArgsUsedInMemWrites.resize(this->LoopCount + 1);
+	this->InArgsUsedInMemWriteByteWidths.resize(this->LoopCount + 1);
+	this->StoppedOnIVMemRangeExprs.resize(this->LoopCount + 1);
+	this->StoppedOnIVNonRangeExprs.resize(this->LoopCount + 1);
+	this->StoppedOnIVMemRangeIterWidths.resize(this->LoopCount + 1);
+	this->StoppedOnIVNonRangeIterWidths.resize(this->LoopCount + 1);
+	this->RelationalLowerBoundExprs.resize(this->LoopCount + 1);
+	this->RelationalUpperBoundExprs.resize(this->LoopCount + 1);
+	this->RelationalMemWriteWidths.resize(this->LoopCount + 1);
+
+	if (!this->HasStructuredControlFlow())
+		return; // just allocate data structures above to avoid crashes, then exit.
+
+	// Prepare for limited interprocedural constant propagation
+	//  by finding constant InArg values.
+	this->ComputeInArgConstValues();
+
+	// Fill in LoopIterationsCountExprs[] for each LoopIndex; emit SENTINEL annotations as discovered along the way.
+	this->BuildLoopIterationCountExprs(VerboseOutput, InfoAnnotFile);
 
 	// See if we had any fatal errors in analysis.
 	for (size_t LoopIndex = 0; LoopIndex < this->GetNumLoops(); ++LoopIndex) {
@@ -18084,6 +18197,7 @@ void SMPFunction::AnalyzeLoopIterations(void) {
 			if (this->DoesLoopWriteMemory(LoopIndex)) {
 				SMP_msg("ERROR: LOOP: Failure to create iteration count expr for loop %d ", LoopIndex);
 				this->DumpFuncNameAndAddr();
+				this->DumpDotCFG();
 			}
 			else {
 				SMP_msg("SERIOUS WARNING: LOOP: Failure to create iteration count expr for non-mem-writing loop %d starting at %llx ",
@@ -20173,7 +20287,7 @@ void SMPFunction::UpdateLoopFollowBlockNum(int LoopHeadBlockNum, int FollowBlock
 			this->DumpFuncNameAndAddr();
 			this->PrintedSPARKUnstructuredMsg = true;
 		}
-		this->HasStructuredCFG = false; // multi-level loop break
+		this->SetHasUnstructuredCFG(); // multi-level loop break
 	}
 
 	if (OldFollowNum == SMP_BLOCKNUM_UNINIT) {
@@ -20388,7 +20502,7 @@ bool SMPFunction::FindLoopContinuePattern(const int BranchBlockNum) {
 			return true;
 		}
 		else {
-			this->HasStructuredCFG = false; // Overlapping loops
+			this->SetHasUnstructuredCFG(); // Overlapping loops
 			if (!this->PrintedSPARKUnstructuredMsg) {
 				SMP_msg("ERROR: SPARK: Unstructured due to Overlapping loops non-single-expr unstructured CFG case at block %d ", BranchBlockNum);
 				this->DumpFuncNameAndAddr();
@@ -20450,6 +20564,8 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 	bool DebugFlag = (0 == strcmp("sub_8063BE0", this->GetFuncName()));
 	string FuncName(this->GetFuncName());
 	bool StartupFunc = IsStartupFuncName(FuncName);
+	bool DeepLoopAnalysesRequested = global_STARS_program->ShouldSTARSPerformDeepLoopAnalyses();
+	bool SPARKTranslationRequested = global_STARS_program->ShouldSTARSTranslateToSPARKAda();
 
 	set<int> NonEscapingRegisterHashes; // memoization optimization: set of register/SSA# hashes that do not reach end of block
 
@@ -20466,12 +20582,12 @@ 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; // Unresolved indirect jump
+		this->SetHasUnstructuredCFG(); // Unresolved indirect jump
 	}
 
 	if (this->HasStructuredControlFlow()) {
 		this->InitializeTCFG();
-		if (global_STARS_program->ShouldSTARSTranslateToSPARKAda()) {
+		if (DeepLoopAnalysesRequested || SPARKTranslationRequested) {
 			this->ComputeTCFGIDoms();
 			this->ComputeTCFGDomFrontiers();
 			this->BuildTCFGDominatorTree();
@@ -20490,13 +20606,13 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 			// Detect special case of a C/C++ loop continue statement. See comments in SMPFunction::FindLoopContinuePattern().
 			bool OverlappingLoops = (CurrBlock->IsLoopHeaderBlock() && CurrBlock->IsLoopTailBlock() && (!CurrBlock->IsSelfLoop()));
 			if (OverlappingLoops) {
-				this->HasStructuredCFG = false; // might handle the loop continue case (SingleExpr) below in future.
+				this->SetHasUnstructuredCFG(); // might handle the loop continue case (SingleExpr) below in future.
 				if (CurrBlock->IsSingleExpression()) {
 					SMP_msg("INFO: Overlapping loops single-expr loop continue special case at block %zu ", BlockIndex);
 					this->DumpFuncNameAndAddr();
 				}
 				else {
-					this->HasStructuredCFG = false; // Overlapping loops
+					this->SetHasUnstructuredCFG(); // Overlapping loops
 					if (!this->PrintedSPARKUnstructuredMsg) {
 						SMP_msg("ERROR: SPARK: Unstructured due to Overlapping loops non-single-expr unstructured CFG case at block %d ", BlockIndex);
 						this->DumpFuncNameAndAddr();
@@ -20512,7 +20628,7 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 				if (CurrInst->IsLoopExitStatement(InvertedExit)) {
 					STARS_ea_t JumpTarget = CurrInst->GetJumpTarget();
 					if ((STARS_BADADDR == JumpTarget) || (!this->IsInstIDInFunc(JumpTarget))) {
-						this->HasStructuredCFG = false; // Bad jump target
+						this->SetHasUnstructuredCFG(); // Bad jump target
 						if (!this->PrintedSPARKUnstructuredMsg) {
 							SMP_msg("ERROR: SPARK: Unstructured due to bad jump target at %llx ", (uint64_t)InstAddr);
 							this->DumpFuncNameAndAddr();
@@ -20522,7 +20638,7 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 					}
 
 					if (this->FindMultiLoopContinue((int) BlockIndex)) {
-						this->HasStructuredCFG = false; // Multi-loop continue
+						this->SetHasUnstructuredCFG(); // Multi-loop continue
 						break; // no point in continuing if we cannot translate to SPARK Ada
 					}
 
@@ -20617,7 +20733,7 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 							this->DumpFuncNameAndAddr();
 							this->PrintedSPARKUnstructuredMsg = true;
 						}
-						this->HasStructuredCFG = false; // Bad jump target
+						this->SetHasUnstructuredCFG(); // Bad jump target
 						break; // no point in continuing if we cannot translate to SPARK Ada
 					}
 					else {
@@ -20647,7 +20763,7 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 		} // end for all blocks
 	} // end if LoopCount > 0 and structured CFG
 
-	if (global_STARS_program->ShouldSTARSTranslateToSPARKAda()) {
+	if (DeepLoopAnalysesRequested || SPARKTranslationRequested) {
 		for (size_t LoopNum = 0; LoopNum < this->GetNumLoops(); ++LoopNum) {
 			if (1 < this->LoopExitTargets[LoopNum].size()) {
 				set<int> DummySet;
@@ -20656,7 +20772,7 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 			}
 		}
 		if (!this->HasGoodLoopFollowBlocks) {
-			this->HasStructuredCFG = false; // Bad loop follow blocks
+			this->SetHasUnstructuredCFG(); // Bad loop follow blocks
 			SMP_msg("ERROR: SPARK: Function %s is unstructured due to bad loop follow blocks.\n",
 				this->GetFuncName());
 		}
@@ -20669,7 +20785,7 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 					if (CurrTCFGBlock->HasIndirectJump()) {
 						bool StructuredSwitch = this->AnalyzeSwitchStatement(CurrTCFGBlock);
 						if (!StructuredSwitch) {
-							this->HasStructuredCFG = false; // Unstructured switch
+							this->SetHasUnstructuredCFG(); // Unstructured switch
 							if (!this->PrintedSPARKUnstructuredMsg) {
 								SMP_msg("ERROR: SPARK: Unstructured due to unstructured switch statements ");
 								this->DumpFuncNameAndAddr();
@@ -20687,7 +20803,7 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 			if (this->HasStructuredControlFlow()) {
 				bool StructuredConditionals = this->AnalyzeConditionalStatements();
 				if (!StructuredConditionals) {
-					this->HasStructuredCFG = false; // Unstructured conditionals
+					this->SetHasUnstructuredCFG(); // Unstructured conditionals
 					if (!this->PrintedSPARKUnstructuredMsg) {
 						SMP_msg("ERROR: SPARK: Unstructured due to miscellaneous CondFollowNode error ");
 						this->PrintedSPARKUnstructuredMsg = true;
@@ -20716,8 +20832,7 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 	//  is unrolled and the entire function is a hash.
 #define STARS_MIN_HASH_BLOCK_SIZE 20
 
-	for (BlockIter = this->Blocks.begin(); BlockIter != this->Blocks.end(); ++BlockIter) {
-		SMPBasicBlock *CurrBlock = (*BlockIter);
+	for (SMPBasicBlock *CurrBlock : this->Blocks) {
 		int BlockNum = CurrBlock->GetNumber();
 #if 0
 		if (CurrBlock->IsLoopTailBlock() && CurrBlock->IsLoopHeaderBlock()) {
@@ -20783,6 +20898,86 @@ void SMPFunction::MarkSpecialNumericErrorCases(void) {
 
 	NonEscapingRegisterHashes.clear();
 
+	if ((0 < this->GetNumLoops()) && this->HasStructuredControlFlow()) {
+		// See if any loop exiting blocks are short circuit conditional expressions,
+		//  and fill in the flag in the loop exiting block info.
+		// See if a loop BIV is used in the compare or test or decrement inst, fill in flag.
+		for (size_t LoopIndex = 0; LoopIndex < this->GetNumLoops(); ++LoopIndex) {
+			for (size_t ExitInfoIndex = 0; ExitInfoIndex < this->LoopExitingBlocksVector[LoopIndex].size(); ++ExitInfoIndex) {
+				if (this->HasShortCircuitConditional()) {
+					int ExitingBlockNum = this->LoopExitingBlocksVector[LoopIndex][ExitInfoIndex].ExitingBlockNum;
+					assert(0 <= ExitingBlockNum);
+					STARSCFGBlock *ExitingCFGBlock = this->GetCFGBlockByNum((size_t)ExitingBlockNum);
+					bool ShortCircuitBlock = ExitingCFGBlock->IsCoalesced() || ExitingCFGBlock->IsExprHeadBlock();
+					this->LoopExitingBlocksVector[LoopIndex][ExitInfoIndex].ShortCircuitExpr = ShortCircuitBlock;
+				}
+
+				STARSInductionVarFamilyIter ListIter;
+				size_t FamilyIndex;
+				SMPInstr *CompareOrTestInst = this->LoopExitingBlocksVector[LoopIndex][ExitInfoIndex].CompareTestDecInst;
+				if (nullptr != CompareOrTestInst) {
+					if (CompareOrTestInst->IsDecrementRTL()) {
+						STARSDefUseIter DefIter = CompareOrTestInst->GetFirstNonFlagsDef(); // really a DecInst
+						assert(DefIter != CompareOrTestInst->GetLastDef());
+						STARSOpndTypePtr DefOp = DefIter->GetOp();
+						if (this->IsLoopInductionVarForAnySSANum(LoopIndex, DefOp, ListIter, FamilyIndex)) {
+							this->LoopExitingBlocksVector[LoopIndex][ExitInfoIndex].ReferencesBIV = true;
+						}
+					}
+					else {
+						for (STARSDefUseConstIter UseIter = CompareOrTestInst->GetFirstConstUse(); UseIter != CompareOrTestInst->GetLastConstUse(); ++UseIter) {
+							STARSOpndTypePtr UseOp = UseIter->GetOp();
+							if (this->IsLoopInductionVarForAnySSANum(LoopIndex, UseOp, ListIter, FamilyIndex)) {
+								this->LoopExitingBlocksVector[LoopIndex][ExitInfoIndex].ReferencesBIV = true;
+								break;
+							}
+						} // end for all USEs
+					}
+				}
+			} // end for all ExitInfo structs for current loop
+		} // end for all loops
+	}
+
+	// See which loops have exactly one good candidate ExitBlockInfo entries.
+	for (size_t LoopIndex = 0; LoopIndex < this->GetNumLoops(); ++LoopIndex) {
+		uint32_t GoodCount = 0; // not ShortCircuit, traces back to compare or test or decrement inst
+		uint32_t VeryGoodCount = 0; // same, but also references a loop BIV
+		bool VeryGoodCandidateFound = false;
+		for (const struct LoopExitingBlockInfo CurrExitInfo : this->LoopExitingBlocksVector[LoopIndex]) {
+			if ((nullptr != CurrExitInfo.CompareTestDecInst) && (!CurrExitInfo.ShortCircuitExpr)) {
+				++GoodCount;
+				if (CurrExitInfo.ReferencesBIV) {
+					++VeryGoodCount;
+					if (!VeryGoodCandidateFound) {
+						VeryGoodCandidateFound = true;
+						// We will use the first very good candidate.
+						if (this->LoopTestBlocksByLoopNum[LoopIndex] != CurrExitInfo.ExitingBlockNum) {
+							SMP_msg("INFO: LOOP: Changing loop test block from %d to %d in loop %zu ",
+								this->LoopTestBlocksByLoopNum[LoopIndex], CurrExitInfo.ExitingBlockNum, LoopIndex);
+							this->DumpFuncNameAndAddr();
+							this->DumpDotCFG();
+							this->LoopTestBlocksByLoopNum[LoopIndex] = CurrExitInfo.ExitingBlockNum;
+							if (this->LoopHeadBlockNumbers[LoopIndex] == CurrExitInfo.ExitingBlockNum) {
+								this->LoopTypesByLoopNum[LoopIndex] = STARS_TOP_TESTING_LOOP;
+							}
+							else if (this->GetBlockByNum((size_t)CurrExitInfo.ExitingBlockNum)->IsLoopTailBlock()) {
+								this->LoopTypesByLoopNum[LoopIndex] = STARS_BOTTOM_TESTING_LOOP;
+							}
+							else {
+								this->LoopTypesByLoopNum[LoopIndex] = STARS_INFINITE_OR_MIDDLE_TESTING_LOOP;
+							}
+						}
+					}
+				}
+			}
+		} // end for all ExitInfo structs for current loop
+		if ((1 != GoodCount) || (1 != VeryGoodCount)) {
+			SMP_msg("WARNING: LOOP: Good candidate ExitBlockInfo count is %lu VeryGood count is %lu for loop %zu ",
+				GoodCount, VeryGoodCount, LoopIndex);
+			this->DumpFuncNameAndAddr();
+		}
+	} // end for all loops
+
 	return;
 } // end of SMPFunction::MarkSpecialNumericErrorCases()
 
@@ -20800,7 +20995,7 @@ void SMPFunction::MarkLoopContinueCases(const SMPBasicBlock *CurrBlock, const in
 			SMP_msg("WARNING: SPARK: LOOP_CONTINUE case detected in block %d FollowBlock %d loop %d ",
 				CurrBlock->GetNumber(), FollowBlockNum, LoopIndex);
 			this->DumpFuncNameAndAddr();
-			this->HasStructuredCFG = false; // loop continue detected
+			this->SetHasUnstructuredCFG(); // loop continue detected
 			this->DumpDotCFG();
 			this->SetControlFlowType(InstAddr, LOOP_CONTINUE);
 		}
@@ -20816,7 +21011,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; // fall-through to next func
+		this->SetHasUnstructuredCFG(); // fall-through to next func
 		if (!this->PrintedSPARKUnstructuredMsg) {
 			SMP_msg("ERROR: SPARK: Unstructured due to fall-through from %llx is not in function ",
 				(uint64_t)InstAddr);
@@ -22027,8 +22222,10 @@ void SMPFunction::EmitAnnotations(FILE *AnnotFile, FILE *InfoAnnotFile) {
 		return;
 	} // end if reduced analysis
 
+#if 0 // Move to Phase 7A
 	// Find and mark special cases that will affect the integer error and other security annotations.
 	this->MarkSpecialNumericErrorCases();
+#endif
 
 	// Emit program CFG xref/indirect branch target annotations.
 	if (this->FuncReturnsToCaller() && this->AreReturnTargetsComputed()) {
@@ -23195,7 +23392,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; // branch outside func
+			this->SetHasUnstructuredCFG(); // branch outside func
 		}
 
 		if (HasLoops && CurrBlock->HasMemoryWrite() && this->IsBlockInAnyLoop((int) BlockNum)) {
diff --git a/src/base/SMPProgram.cpp b/src/base/SMPProgram.cpp
index d16a4af0cb14583737b162f086fafaf78b1d3e4a..d7a627bd374fed5b04d1cc9c9817e359e21ebc0e 100644
--- a/src/base/SMPProgram.cpp
+++ b/src/base/SMPProgram.cpp
@@ -895,6 +895,25 @@ void SMPProgram::Analyze(ProfilerInformation *pi, FILE *AnnotFile, FILE *InfoAnn
 	SMP_msg("INFO: TIME: Phase 7: ReturnTargets + InterproceduralTypes + InArgTypes + TraceInArgs: %7.2f\n", TimeDiff);
 	SMP_msg("INFO: VMEM: Phase 7: Maximum resident memory usage in MB: %ld \n", global_stars_interface->GetMemoryInUse());
 
+	// Loop 7A: MarkSpecialNumericErrorCases(), including SPARK structured analysis.
+	// Find and mark special cases that will affect the integer error and other security annotations.
+	Time4 = time(nullptr);
+	if (global_STARS_program->ShouldSTARSPerformDeepLoopAnalyses()) {
+		for (FuncListIter = this->PrioritizedFuncList.begin(); FuncListIter != this->PrioritizedFuncList.end(); ++FuncListIter) {
+			CurrFunc = (*FuncListIter);
+			if (nullptr == CurrFunc) {
+				SMP_msg("ERROR: NULL Func ptr in PrioritizedFuncList\n");
+				continue;
+			}
+			if (CurrFunc->StackPtrAnalysisSucceeded() && CurrFunc->HasGoodRTLs()) {
+				CurrFunc->MarkSpecialNumericErrorCases();
+			}
+		}
+	}
+	Time5 = time(nullptr);
+	TimeDiff = difftime(Time5, Time4);
+	SMP_msg("INFO: TIME: Phase 7A: MarkSpecialNumericErrorCases+StructuralAnalysis: %7.2f \n", TimeDiff);
+	SMP_msg("INFO: VMEM: Phase 7A: Maximum resident memory usage in MB: %ld \n", global_stars_interface->GetMemoryInUse());
 
 	// Loop 7B: Loop iteration and memory access analysis.
 	Time4 = time(nullptr);
@@ -905,9 +924,9 @@ void SMPProgram::Analyze(ProfilerInformation *pi, FILE *AnnotFile, FILE *InfoAnn
 				SMP_msg("ERROR: NULL Func ptr in PrioritizedFuncList\n");
 				continue;
 			}
-				if (CurrFunc->StackPtrAnalysisSucceeded() && CurrFunc->HasGoodRTLs() && (!CurrFunc->HasUnresolvedIndirectJumps())) {
-					CurrFunc->AnalyzeLoopIterations();
-				}
+			if (CurrFunc->StackPtrAnalysisSucceeded() && CurrFunc->HasGoodRTLs() && (!CurrFunc->HasUnresolvedIndirectJumps())) {
+				CurrFunc->AnalyzeLoopIterations();
+			}
 		}
 	}
 	Time5 = time(nullptr);