diff --git a/SConscript b/SConscript
index 114b0264712501db350f0c638144871eb4beef53..2115b55741a7f73ee8b93bfcd51b28ea2a71a475 100644
--- a/SConscript
+++ b/SConscript
@@ -38,38 +38,38 @@ argenv.Replace(SECURITY_TRANSFORMS_HOME=os.environ['SECURITY_TRANSFORMS_HOME'])
 
 
 if argenv['SMPSA_HOME'] is None:
-    print 'Cannot proceed without SMPSA_HOME set.'
+    print('Cannot proceed without SMPSA_HOME set.')
     exit(1)
 
 
 
 if int(argenv['debug']) == 1:
-	print "Setting debug mode"
+	print("Setting debug mode")
 	STARS_CCFLAGS=" -g "
 	STARS_LDFLAGS=""
 	STARS_LDPREFIX=""
 elif int(argenv['debugopt']) == 1:
-	print "Setting debugopt mode"
+	print("Setting debugopt mode")
 	STARS_CCFLAGS=" -g -O1 "
 	STARS_LDFLAGS=""
 	STARS_LDPREFIX=""
 elif int(argenv['debugopt2']) == 1:
-	print "Setting debugopt2 mode"
+	print("Setting debugopt2 mode")
 	STARS_CCFLAGS=" -g -O2 "
 	STARS_LDFLAGS=""
 	STARS_LDPREFIX=""
 elif int(argenv['debugmem']) == 1:
-	print "Setting debugmem mode"
+	print("Setting debugmem mode")
 	STARS_CCFLAGS=" -g -fsanitize=address -fno-omit-frame-pointer "
 	STARS_LDFLAGS=" -lasan "   
 	STARS_LDPREFIX="LD_PRELOAD='/usr/lib/gcc/x86_64-linux-gnu/5/libasan.so'"
 elif int(argenv['profile']) == 1:
-	print "Setting perf profiling mode"
+	print("Setting perf profiling mode")
 	STARS_CCFLAGS=" -O3 -fno-omit-frame-pointer -pg "
 	STARS_LDFLAGS=""   
 	STARS_LDPREFIX=""
 else:
-	print "Setting release mode"
+	print("Setting release mode")
 	STARS_CCFLAGS=" -O2 "
 	STARS_LDFLAGS=""
 	STARS_LDPREFIX=""
@@ -84,7 +84,7 @@ else:
 
 # check both on for error`
 if int(argenv['build_ida7']) == 1 and int(argenv['build_ida']) == 1:
-	print "Cannot set both build_ida7 and build_ida at the same time."
+	print("Cannot set both build_ida7 and build_ida at the same time.")
 	sys.exit(0)
 #check both default
 elif int(argenv['build_ida7']) == -1 and int(argenv['build_ida']) == -1:
@@ -110,7 +110,7 @@ elif int(argenv['build_ida7']) == 0 and int(argenv['build_ida']) == 0:
 	''' okay, nothing to do.'''
 # how can it be none of these?
 else:
-	print "build_ida/build_ida7 set wildly.  values are 0, 1 or left unset. (or, possibly internal error in build?)" 
+	print("build_ida/build_ida7 set wildly.  values are 0, 1 or left unset. (or, possibly internal error in build?)" )
 	sys.exit(0)
 
 if not 'IDAROOT' in os.environ:
@@ -149,28 +149,28 @@ libehp=libehpEnv.SConscript("libehp/SConscript")
 
 if int(argenv['build_ida']) == 1 or int(argenv['build_ida7']) == 1:
 	if argenv['IDASDK'] is None:
-    		print 'Cannot proceed without IDASDK set.'
+    		print('Cannot proceed without IDASDK set.')
     		exit(1)
 	
 	if argenv['IDAROOT'] is None:
-    		print 'Cannot proceed without IDAROOT set.'
+    		print('Cannot proceed without IDAROOT set.')
     		exit(1)
 
 	if argenv['IDASDK'] is None:
-    		print 'Cannot proceed without IDASDK set.'
+    		print('Cannot proceed without IDASDK set.')
     		exit(1)
 	
 	if argenv['IDAROOT'] is None:
-    		print 'Cannot proceed without IDAROOT set.'
+    		print('Cannot proceed without IDAROOT set.')
     		exit(1)
 
 	if int(argenv['build_ida']) == 1:
-		print "Build IDA Plugin"
+		print("Build IDA Plugin")
 		idalib=SConscript('SConscript.ida', variant_dir='build/ida')
 	elif int(argenv['build_ida7']) == 1:
-		print "Build IDA 7.0+ Plugin"
+		print("Build IDA 7.0+ Plugin")
 		idalib=SConscript('SConscript.ida7', variant_dir='build/ida')
-	print "Done build IDA Plugin"
+	print("Done build IDA Plugin")
 
 	Default(idalib)
 	argenv.Depends(idalib, libehp)
@@ -179,9 +179,9 @@ if int(argenv['build_ida']) == 1 or int(argenv['build_ida7']) == 1:
 
 if int(argenv['build_irdb']) == 1 or int(argenv['build_irdb_driver']) == 1:
 	if argenv['SECURITY_TRANSFORMS_HOME'] is None:
-	    print 'Cannot build libstars.a without SECURITY_TRANSFORMS_HOME set.  Did you forget the env. var.?  Or try setting build_irdb=0. '
+	    print('Cannot build libstars.a without SECURITY_TRANSFORMS_HOME set.  Did you forget the env. var.?  Or try setting build_irdb=0. ')
 	    exit(1)
-	print "Build IDA/IRDB library"
+	print("Build IDA/IRDB library")
 	irdblib=SConscript('SConscript.irdb_lib', variant_dir='build/irdb_lib')
 	installers=installers+irdblib
 	Default(irdblib)
diff --git a/SConscript.irdb_lib b/SConscript.irdb_lib
index 8a2168ba8d52080fe4474760499d306fbdc9f457..dca53362d2112b1036012623cadbcbdb2c2e954b 100644
--- a/SConscript.irdb_lib
+++ b/SConscript.irdb_lib
@@ -48,7 +48,7 @@ IRDB_LDFLAGS=" "
 if processor == "x86_64" or processor == "i686" or processor == "i386":
 	# set 32/64 bit build properly
 	if int(argenv['do_64bit_build']) == 2:
-		print "Defaulting to mach-dep 32/64 bit build parameter"
+		print("Defaulting to mach-dep 32/64 bit build parameter")
 
 	elif int(argenv['do_64bit_build']) == 1:
 		IRDB_CCFLAGS+=" -m64 "
diff --git a/cicd_testing/do-build.sh b/cicd_testing/do-build.sh
index 6205583d521f767241ae528d15f40f2f9f091431..0fa3719423a11bf99fbe20260fc34094036d7f20 100755
--- a/cicd_testing/do-build.sh
+++ b/cicd_testing/do-build.sh
@@ -26,7 +26,7 @@ main()
 	local orig_dir=$(pwd)
 
 	# puts peasoup_umbrella (and all submodules) in CICD_MODULE_WORK_DIR
-	cicd_setup_module_dependency allnp/peasoup_umbrella.git cicd_stars_umbrella
+	cicd_setup_module_dependency opensrc/zipr.git cicd_stars_umbrella
 
 
 	# puts the version of zipr to test in cicd_stars_umbrella/SMPStaticAnalyzer.
diff --git a/include/base/SMPBasicBlock.h b/include/base/SMPBasicBlock.h
index 8489cf6ad6d74be1bff9891ca9f0ade9eb081a5c..ada394406ef392128f740ced5e54df0cd19868e5 100644
--- a/include/base/SMPBasicBlock.h
+++ b/include/base/SMPBasicBlock.h
@@ -398,7 +398,7 @@ public:
 	void EmitSPARKAdaForAllInsts(FILE *BodyFile); // Call SMPInstr::EmitSPARKAda() for all insts in block.
 	void EmitSPARKAdaDisasmOnly(FILE *BodyFile); // For coalesced blocks, emit disasm comments so the original code is visible.
 	void EmitSPARKAdaForExpression(FILE *BodyFile); // For SingleExpression block, emit SPARK Ada expression
-	bool EmitSPARKAdaForExprUse(FILE *BodyFile, std::vector<SMPInstr *>::const_reverse_iterator RevInstIter, STARSOpndTypePtr UseOp, int UseSSANum); // Emit SPARK expression for UseOp at RevInstIter
+	bool EmitSPARKAdaForExprUse(FILE *BodyFile, std::vector<SMPInstr *>::const_reverse_iterator RevInstIter, const STARSOpndTypePtr &UseOp, int UseSSANum); // Emit SPARK expression for UseOp at RevInstIter
 
 	// Analysis methods
 	bool AllPredecessorsNumbered(void);
@@ -491,6 +491,7 @@ public:
 	bool MarkTaintWarningInArgs(void); // Trace critical args for critical library calls back to InArgs, if possible. Return true if critical arg traced to InArg.
 	// Is DefOp+DefSSANum (from WorkList head) at DefAddr used as address reg or as source operand in unsafe memory write?
 	bool IsDefUsedInUnsafeMemWrite(std::list<std::pair<std::pair<STARSOpndTypePtr, int>, STARS_ea_t> > &WorkList, const STARSOpndTypePtr &DefOp, int DefSSANum, STARS_ea_t DefAddr);
+	bool IsNextDownwardUseNotByExternalCallInst(const STARSOpndTypePtr &UseRegOp); // Trace downward only; is next USE of UseRegOp not in a CALL-to-linker-stub inst?
 
 	STARS_sval_t ComputeStackAdjustmentAfterCall(STARS_ea_t CallAddr); // find stack pointer adjustment code after call, return stack delta or zero
 	STARS_ea_t FindFixedCallFallThrough(void) const; // Find the push operand that passed the fall-through address to a fixed call
@@ -582,7 +583,7 @@ private:
 	STARSOpndSetIter EraseLiveOut(STARSOpndSetIter LiveOutIter);
 	STARSOpndSetIter EraseUpExposed(STARSOpndSetIter UpExposedIter);
 	STARSOpndSetIter EraseVarKill(STARSOpndSetIter VarKillIter);
-	void EmitSPARKAdaExprHelper(FILE *BodyFile, SMPInstr *CompareInst, const STARSOpndTypePtr LeftOp, const STARSOpndTypePtr LeftOpNoNorm, const bool HeaderBlock, const bool UseFP);
+	void EmitSPARKAdaExprHelper(FILE *BodyFile, SMPInstr *CompareInst, const STARSOpndTypePtr &LeftOp, const STARSOpndTypePtr &LeftOpNoNorm, const bool HeaderBlock, const bool UseFP);
 	std::set<SMPPhiFunction, LessPhi>::iterator InferPhiDefType(std::set<SMPPhiFunction, LessPhi>::iterator DefPhi, bool &changed); // infer, propagate to all uses
 #if STARS_BUILD_DEF_USE_CHAINS
 	unsigned int GetLocalDUIndex(STARSOpndTypePtr DefOp, int SSANum);
diff --git a/include/base/SMPDataFlowAnalysis.h b/include/base/SMPDataFlowAnalysis.h
index f1f764a037f7894b1cf16d3ef082071bfc8bd7df..ecb88e94176b3cbb9cf5a4491ae71286e57ac9f8 100644
--- a/include/base/SMPDataFlowAnalysis.h
+++ b/include/base/SMPDataFlowAnalysis.h
@@ -837,7 +837,8 @@ public:
 	inline std::set<DefOrUse, LessDefUse>::const_iterator GetFirstConstRef(void) const { return Refs.cbegin(); };
 	inline std::set<DefOrUse, LessDefUse>::const_iterator GetLastConstRef(void) const { return Refs.cend(); };
 	std::set<DefOrUse, LessDefUse>::iterator FindRef(const STARSOpndTypePtr &SearchOp);
-	
+	std::set<DefOrUse, LessDefUse>::const_iterator FindConstRef(const STARSOpndTypePtr &SearchOp) const;
+
 	// Set methods
 	// Insert a new DEF or USE; must be new, insert must succeed else we assert.
 	std::set<DefOrUse, LessDefUse>::iterator InsertRef(DefOrUse Ref); 
diff --git a/include/base/SMPInstr.h b/include/base/SMPInstr.h
index 3d178df186bb9745205dd86013971a7081473bc6..8dd19acfc8608aa62d8310933594cd3849886e3c 100644
--- a/include/base/SMPInstr.h
+++ b/include/base/SMPInstr.h
@@ -213,7 +213,7 @@ extern const char *OperatorText[]; // for printing operators in Dump() methods a
 void PrintOperandSPARKAdaSuffix(const STARSOpndTypePtr &Opnd, FILE *OutFile);
 
 // Print an operator in SPARK-Ada form.
-void PrintSPARKAdaOperator(SMPoperator Oper, std::string &OutString, bool &PrefixProcCall, bool &PrefixUnary, bool ConstFollows = false);
+void PrintSPARKAdaOperator(SMPoperator Oper, std::string &OutString, bool &PrefixProcCall, bool &PrefixUnary, bool ConstFollows, bool ShortCircuitExpr = false);
 
 // Print current indentation level using tabs.
 void PrintSPARKIndentTabs(FILE *OutFile);
@@ -821,6 +821,8 @@ public:
 
 	// Query methods
 	inline bool RegOpndMatches(std::size_t OpndNum, STARS_regnum_t RegNum) const { return STARSInstPtr->RegOpndMatches(OpndNum, RegNum); };
+	inline bool IsOpndUsed(const STARSOpndTypePtr &CurrOp) const { return (Uses.FindConstRef(CurrOp) != Uses.GetLastConstRef()); };
+	inline bool IsOpndDefined(const STARSOpndTypePtr &CurrOp) const { return (Defs.FindConstRef(CurrOp) != Defs.GetLastConstRef()); };
 	bool HasDestMemoryOperand(void) const; // Does instruction write to memory?
 	bool HasSourceMemoryOperand(void) const; // Does instruction read from memory?
 	inline bool HasIndirectMemoryWrite(void) const { return (booleans2 & INSTR_SET_INDIRECT_MEM_WRITE); };
diff --git a/include/interfaces/idapro/STARSInstruction.h b/include/interfaces/idapro/STARSInstruction.h
index 4b9e11e249986bd37384c7cb068cdae0381b5a75..3c564e4b742d7dd2b9ce94dc838441f5319bdc00 100644
--- a/include/interfaces/idapro/STARSInstruction.h
+++ b/include/interfaces/idapro/STARSInstruction.h
@@ -80,6 +80,8 @@ class STARS_IDA_Instruction_t : public STARS_Instruction_t
 		// Constructors and destructors
 		STARS_IDA_Instruction_t(const STARS_InstructionID_t& p_id) : STARSCmd({}), STARS_Instruction_t(p_id), ImplicitDEFs(false) {
 			if (STARS_IsSSAMarkerPseudoID(p_id.GetIDWithinFile())) { // SSA marker pseudo-inst
+				// (void) memset(&(STARScmd), 0, sizeof(STARScmd));
+				STARScmd=STARS_IDA_insn_t{};
 				STARScmd.itype = NN_fnop;
 				STARScmd.size = 1;
 			}
diff --git a/libehp b/libehp
index 7afdf11de50040c19e62e3f07ce1f52b463e6e73..3c4aa12b45fe33486d0efc89a5dd3430e03b4051 160000
--- a/libehp
+++ b/libehp
@@ -1 +1 @@
-Subproject commit 7afdf11de50040c19e62e3f07ce1f52b463e6e73
+Subproject commit 3c4aa12b45fe33486d0efc89a5dd3430e03b4051
diff --git a/src/base/SMPBasicBlock.cpp b/src/base/SMPBasicBlock.cpp
index 225b8c5cc650e962259df7158fc54e02c4ebe716..4093f8b6decb04ee867675c7dfd6187ef43a465a 100644
--- a/src/base/SMPBasicBlock.cpp
+++ b/src/base/SMPBasicBlock.cpp
@@ -686,7 +686,7 @@ void SMPBasicBlock::EmitSPARKAdaDisasmOnly(FILE *BodyFile) {
 }
 
 // Factored-out operand emitter.
-void SMPBasicBlock::EmitSPARKAdaExprHelper(FILE *BodyFile, SMPInstr *CompareInst, const STARSOpndTypePtr LeftOp, const STARSOpndTypePtr LeftOpNoNorm, const bool HeaderBlock, const bool UseFP) {
+void SMPBasicBlock::EmitSPARKAdaExprHelper(FILE *BodyFile, SMPInstr *CompareInst, const STARSOpndTypePtr &LeftOp, const STARSOpndTypePtr &LeftOpNoNorm, const bool HeaderBlock, const bool UseFP) {
 	if (LeftOp->IsImmedOp() || HeaderBlock) {
 		if (!LeftOp->IsImmedOp()) {
 			CompareInst->PrintSPARKAdaOperand(LeftOpNoNorm, BodyFile, false, UseFP, true, false);
@@ -706,7 +706,8 @@ void SMPBasicBlock::EmitSPARKAdaExprHelper(FILE *BodyFile, SMPInstr *CompareInst
 			SMP_fprintf(BodyFile, "ERROR in compare operand\n");
 		}
 	}
-}
+	return;
+} // end of SMPBasicBlock::EmitSPARKAdaExprHelper()
 
 
 // For SingleExpression block, emit SPARK Ada expression
@@ -719,6 +720,46 @@ void SMPBasicBlock::EmitSPARKAdaForExpression(FILE *BodyFile) {
 	STARSCFGBlock *CurrCFGBlock = this->GetFunc()->GetClonedCFGBlockByNum((size_t)TCFGBlockNum);
 	bool HeaderBlock = (!CurrCFGBlock->IsCoalesced());
 
+	// Emit the SPARK Ada for the left operand of the comparison.
+	// First, set up iterators and pointers.
+	std::vector<SMPInstr *>::const_reverse_iterator RevInstIter = this->GetRevInstCBegin();
+	SMPInstr *LastInst = (*RevInstIter);
+	bool UnsignedBranchOpcode = LastInst->MDIsUnsignedBranch();
+	bool SignBitSetBranch = LastInst->MDIsBranchOnSignBit();
+	bool SignBitNotSetBranch = LastInst->MDIsBranchOnNotSignBit();
+
+	// If this is the HeaderBlock, then we start with a simple reference to the flag
+	//  register, which has been set based on operations in the HeaderBlock before the
+	//  last inst. This approach is simple, avoids problems with cases that don't have
+	//  a compare or test instruction but set the flag in another operation, and avoids
+	//  erroneous code when instruction scheduling does something like:
+	//
+	//  test rax,rax
+	//  mov rax,rbx  ; does not affect flags set by previous inst, overwrites rax
+	//  jz label
+	//
+	//  If generate "if (X86.RAX \= 0)" then the SPARK Ada code will be using the copy
+	//  of RBX that was put into RAX by the instruction-scheduled move opcode. Incorrect.
+	if (HeaderBlock) {
+		assert(this->HasConditionalBranch());
+		bool NegateLeft = CurrCFGBlock->GetExpr()->IsLeftExprNegated();
+		if (NegateLeft) {
+			SMP_fprintf(BodyFile, "(not ");
+		}
+		LastInst->MDEmitSPARKAdaCondition(BodyFile);
+		if (NegateLeft) {
+			SMP_fprintf(BodyFile, ") ");
+		}
+
+		// Mark all instructions in the single-expr block as translated.
+		for (SMPInstr *CurrInst : this->InstVec) {
+			CurrInst->SetSPARKTranslated(true);
+		}
+		this->IncrementSPARKTranslationCount();
+		return;
+	}
+
+
 	// We will divide into cases: Expression block can end in signed compare instruction or
 	//  unsigned compare (bitwise AND) instruction, and unsigned compare is often to itself
 	//  to test for zero or non-zero value.
@@ -736,14 +777,6 @@ void SMPBasicBlock::EmitSPARKAdaForExpression(FILE *BodyFile) {
 	bool SignedCompareCase = (SMP_S_COMPARE == CompareOperator);
 	bool UnsignedSelfCompareCase = ((SMP_U_COMPARE == CompareOperator) && IsEqOp(CompareRT->GetConstRightOperandNoNorm(), CompareRT->GetConstLeftOperandNoNorm()));
 
-	// Emit the SPARK Ada for the left operand of the comparison.
-	// First, set up iterators and pointers.
-	std::vector<SMPInstr *>::const_reverse_iterator RevInstIter = GetRevInstCBegin();
-	SMPInstr *LastInst = (*RevInstIter);
-	bool UnsignedBranchOpcode = LastInst->MDIsUnsignedBranch();
-	bool SignBitSetBranch = LastInst->MDIsBranchOnSignBit();
-	bool SignBitNotSetBranch = LastInst->MDIsBranchOnNotSignBit();
-
 	// CompareInst might be in this block or in a previous block.
 	STARS_ea_t CompareAddr = CompareInst->GetAddr();
 	SMPBasicBlock *CompareBlock;
@@ -881,15 +914,15 @@ void SMPBasicBlock::EmitSPARKAdaForExpression(FILE *BodyFile) {
 	}
 
 	// Mark all instructions in the single-expr block as translated.
-	for (vector<SMPInstr *>::iterator InstIter = this->GetFirstInst(); InstIter != this->GetLastInst(); ++InstIter) {
-		(*InstIter)->SetSPARKTranslated(true);
+	for (SMPInstr *CurrInst : this->InstVec) {
+		CurrInst->SetSPARKTranslated(true);
 	}
 	this->IncrementSPARKTranslationCount();
 	return;
 } // end of SMPBasicBlock::EmitSPARKAdaForExpression()
 
 // Emit SPARK expression for *UseIter at RevInstIter
-bool SMPBasicBlock::EmitSPARKAdaForExprUse(FILE *BodyFile, vector<SMPInstr *>::const_reverse_iterator RevInstIter, STARSOpndTypePtr UseOp, int UseSSANum) {
+bool SMPBasicBlock::EmitSPARKAdaForExprUse(FILE *BodyFile, vector<SMPInstr *>::const_reverse_iterator RevInstIter, const STARSOpndTypePtr &UseOp, int UseSSANum) {
 	// Search backwards in this block for DEF of UseIter operand. If not found,
 	//  just print UseIter operand. If DEF found, recursively follow and print ultimate DEF expression.
 	bool Printed = false;
@@ -953,12 +986,8 @@ bool SMPBasicBlock::EmitSPARKAdaForExprUse(FILE *BodyFile, vector<SMPInstr *>::c
 				bool PrefixUnaryOperator = false;
 				bool ConstFollows = (!DefRT->HasRightSubTree()) && DefRT->GetConstRightOperandNoNorm()->IsImmedOp();
 				SMPoperator DefRTOperator = DefRT->GetOperator();
-				PrintSPARKAdaOperator(DefRTOperator, OperatorString, OperatorIsProcCall, PrefixUnaryOperator, ConstFollows);
-				if (OperatorIsProcCall) {
-					SMP_fprintf(BodyFile, "ERROR ");
-					return true;
-				}
-				if (PrefixUnaryOperator) {
+				PrintSPARKAdaOperator(DefRTOperator, OperatorString, OperatorIsProcCall, PrefixUnaryOperator, ConstFollows, true);
+				if (PrefixUnaryOperator || OperatorIsProcCall) {
 					SMP_fprintf(BodyFile, "%s(", OperatorString.c_str());
 				}
 				else {
@@ -980,13 +1009,19 @@ bool SMPBasicBlock::EmitSPARKAdaForExprUse(FILE *BodyFile, vector<SMPInstr *>::c
 					SMP_fprintf(BodyFile, ") ");
 				}
 				else { // Have tracked & printed DefLeftOp; now print infix operator, then right-hand-side.
-					SMP_fprintf(BodyFile, " %s ", OperatorString.c_str());
+					if (!OperatorIsProcCall) { // Proc call is already printed; not infix
+						SMP_fprintf(BodyFile, " %s ", OperatorString.c_str());
+					}
 					if ((SMP_DECREMENT == DefRTOperator) || (SMP_INCREMENT == DefRTOperator)) {
 						Printed = true; // Operator string was +1 or -1; no right operand
 						SMP_fprintf(BodyFile, ") ");
 					}
 					else {
 						// If we have yet another right tree, terminate the tracking by printing it.
+						if (OperatorIsProcCall) {
+							// Separate left and right operands with a comma.
+							SMP_fprintf(BodyFile, ", ");
+						}
 						if (DefRT->HasRightSubTree()) {
 							SMP_fprintf(BodyFile, " (");
 							DefRT->EmitSPARKAdaForRHS(BodyFile, true);
@@ -2559,9 +2594,7 @@ void SMPBasicBlock::SCCPGlobalPropagationHelper(const STARSOpndTypePtr &GlobalOp
 	}
 	else if (this->IsUpExposed(GlobalOp)) { // case 2
 		FoundReDEF = false;
-		vector<SMPInstr *>::iterator InstIter;
-		for (InstIter = this->GetFirstInst(); InstIter != this->GetLastInst(); ++InstIter) {
-			SMPInstr *CurrInst = (*InstIter);
+		for (SMPInstr *CurrInst : this->InstVec) {
 			set<DefOrUse, LessDefUse>::iterator UseIter = CurrInst->FindUse(GlobalOp);
 			if (UseIter != CurrInst->GetLastUse()) { // operand is USEd; check SSANum
 				int UseSSANum = UseIter->GetSSANum();
@@ -5184,8 +5217,7 @@ bool SMPBasicBlock::IsDefOnlyUsedAsAddressReg(STARS_ea_t DefAddr, const STARSOpn
 		vector<SMPInstr *>::iterator InstIter;
 		STARSOpndTypePtr SearchOp = DefOp;
 		set<DefOrUse, LessDefUse>::iterator UseIter;
-		for (InstIter = this->GetFirstInst(); InstIter != this->GetLastInst(); ++InstIter) {
-			SMPInstr *CurrInst = (*InstIter);
+		for (SMPInstr *CurrInst : this->InstVec) {
 			STARS_ea_t InstAddr = CurrInst->GetAddr();
 			if (CurrInst->IsMarkerInst())
 				continue;
@@ -5282,8 +5314,7 @@ bool SMPBasicBlock::IsDefUsedInLoopCompareAndBranch(STARS_ea_t DefAddr, const ST
 
 	set<DefOrUse, LessDefUse>::iterator UseIter;
 	bool FoundDefAddrInst = false;
-	for (InstIter = this->GetFirstInst(); InstIter != this->GetLastInst(); ++InstIter) {
-		SMPInstr *CurrInst = (*InstIter);
+	for (SMPInstr *CurrInst : this->InstVec) {
 		STARS_ea_t InstAddr = CurrInst->GetAddr();
 		if (CurrInst->IsMarkerInst())
 			continue;
@@ -5489,6 +5520,41 @@ bool SMPBasicBlock::FindSingleExpression(void) {
 		} // end while reverse inst iteration
 	} // end if COND_BRANCH for LastInst
 
+	// Don't classify as single-expr if the block has register side effects.
+	if (FoundSingleExpr) {
+		for (STARSOpndTypePtr KillOp : this->KillSet) {
+			assert(KillOp->IsRegOp());
+			if (this->IsLiveOut(KillOp)) {
+				// We make one exception. The DEADREGS annotations are conservative, partly depending on
+				//  the addition of numerous registers to the USE and DEF lists for external (linker-resolved)
+				//  function calls. In particular, it is probably too conservative to assume that the register
+				//  used for func return values is a USE of the external func (e.g. RAX in X86). 
+				//  We don't want to trust the LiveOut status of the return reg; we want to see if is next use
+				//  on all paths out of the current block is for a CALL to an external func. If so, it is not
+				//  sufficient cause to invalidate our SingleExpr determination.
+				bool ReturnValueReg = (MD_RETURN_VALUE_REG == KillOp->GetReg());
+				bool InvalidatingUse = false;
+				if (ReturnValueReg) {
+					int CurrBlockNum = this->GetNumber();
+					for (SMPBasicBlock *SuccBlock : this->GetConstSuccList()) {
+						// bool BackEdge = (SuccBlock->GetNumber() <= CurrBlockNum);
+						if (SuccBlock->IsLiveIn(KillOp)) { // Only LiveIn paths are worth following.
+							this->GetFunc()->ResetProcessedBlocks();
+							InvalidatingUse = SuccBlock->IsNextDownwardUseNotByExternalCallInst(KillOp);
+							if (InvalidatingUse)
+								break; // Any non-call-to-linker-stub use is final failure for this search.
+						}
+					} // end for all successor blocks
+				}
+				if ((!ReturnValueReg) || InvalidatingUse) {
+					FoundSingleExpr = false;
+					SMP_msg("WARNING: SPARK: SingleExpr block %d invalidated due to LiveOut reg %s ", this->GetNumber(), MDGetRegName(KillOp));
+					this->GetFunc()->DumpFuncNameAndAddr();
+				}
+			}
+		} // end for all KillSet operands
+	}
+
 	return FoundSingleExpr;
 } // end of SMPBasicBlock::FindSingleExpression()
 
@@ -8071,6 +8137,62 @@ bool SMPBasicBlock::IsDefUsedInUnsafeMemWrite(list<pair<pair<STARSOpndTypePtr, i
 	return FoundMemWriteUse;
 } // end of SMPBasicBlock::IsDefUsedInUnsafeMemWrite()
 
+// Trace downward only; is next USE of UseRegOp not in a CALL-to-linker-stub inst?
+bool SMPBasicBlock::IsNextDownwardUseNotByExternalCallInst(const STARSOpndTypePtr &UseRegOp) {
+	bool FoundNonCallUse = false;
+	bool FoundCallUse = false;
+	bool UseSeen = false;
+	bool RedefinedByCallee = false; // could be used to allow pass-through of non-linker-stub-call with no redef; dangerous
+	int CurrBlockNum = this->GetNumber();
+	if (!this->IsProcessed()) {
+		this->SetProcessed(true);
+		if (this->IsUpExposed(UseRegOp)) { // must be used in an inst in this block
+			for (SMPInstr *CurrInst : this->InstVec) {
+				if (CurrInst->IsOpndUsed(UseRegOp)) {
+					UseSeen = true;
+					FoundCallUse = (CALL == CurrInst->GetDataFlowType());
+					if (FoundCallUse) {
+						// Internal calls have actual analysis of USEs, not just assumptions.
+						//  We want to accept their USE of a register as precise, but not
+						//  the pseudo-USEs by external (linker-resolved) calls.
+						STARS_ea_t CallTargetAddr = CurrInst->GetCallTarget();
+						FoundCallUse = (STARS_BADADDR != CallTargetAddr);
+						if (FoundCallUse) {
+							SMPFunction *TargetFunc = this->GetFunc()->GetProg()->FindFunction(CallTargetAddr);
+							FoundCallUse = ((nullptr != TargetFunc) && TargetFunc->IsLinkerStub());
+							RedefinedByCallee = CurrInst->IsOpndDefined(UseRegOp);
+						}
+					}
+					if (!FoundCallUse) {
+						FoundNonCallUse = true;
+						SMP_msg("INFO: SPARK: IsNextDownwardUseNotByExternalCallInst() returns true due to use at %llx of reg %s ",
+							(uint64_t)CurrInst->GetAddr(), RegNames[(size_t)UseRegOp->GetReg()]);
+						this->GetFunc()->DumpFuncNameAndAddr();
+					}
+					break;
+				}
+			} // end for all insts in block
+			assert(UseSeen); // UpExposed implies USE within block
+		}
+
+		if (!UseSeen && this->IsLiveOut(UseRegOp) && (!this->IsVarKill(UseRegOp))) { // pass-through case
+			// Recurse into successors
+			for (SMPBasicBlock *SuccBlock : this->GetConstSuccList()) {
+				// bool BackEdge = (CurrBlockNum >= SuccBlock->GetNumber());
+				if (SuccBlock->IsLiveIn(UseRegOp)) {
+					bool SuccNonCallUse = SuccBlock->IsNextDownwardUseNotByExternalCallInst(UseRegOp);
+					FoundNonCallUse = SuccNonCallUse;
+					if (SuccNonCallUse) {
+						break; // one true path makes final result true
+					}
+				}
+			} // end for all successor blocks
+		}
+	}
+
+	return FoundNonCallUse;
+} // end of SMPBasicBlock::IsNextDownwardUseByExternalCallInst()
+
 // recursive allocation/copy of subexprs into new expr.
 STARSCondExpr *STARSCondExpr::DeepCopyExpr(void) {
 	STARSCondExpr *NewExpr = new STARSCondExpr(*this);
@@ -8127,7 +8249,11 @@ void STARSCondExpr::EmitSPARKAdaShortCircuitExpr(FILE *BodyFile, const bool Inve
 	}
 	else {
 		// Recurse into LeftExpr
+		// Ada puts "or else" and "and then" at same precedence level; they cannot be
+		//  mixed without parentheses, so we parenthesize when recursing into subexprs.
+		SMP_fprintf(BodyFile, "(");
 		this->GetLeftExpr()->EmitSPARKAdaShortCircuitExpr(BodyFile, false);
+		SMP_fprintf(BodyFile, ")");
 	}
 	if (this->NegateLeftExpr) { // close "not" parenthesis
 		SMP_fprintf(BodyFile, ") ");
@@ -8157,7 +8283,9 @@ void STARSCondExpr::EmitSPARKAdaShortCircuitExpr(FILE *BodyFile, const bool Inve
 	}
 	else {
 		// Recurse into RightExpr
+		SMP_fprintf(BodyFile, "(");
 		this->GetRightExpr()->EmitSPARKAdaShortCircuitExpr(BodyFile, false);
+		SMP_fprintf(BodyFile, ")");
 	}
 
 	return;
diff --git a/src/base/SMPDataFlowAnalysis.cpp b/src/base/SMPDataFlowAnalysis.cpp
index d7a0acfc9a1418e04ec310d5e1698bdb5e20d1cd..804912881be695056d69cfc6fcf892333151d116 100644
--- a/src/base/SMPDataFlowAnalysis.cpp
+++ b/src/base/SMPDataFlowAnalysis.cpp
@@ -3215,6 +3215,14 @@ set<DefOrUse, LessDefUse>::iterator DefOrUseSet::FindRef(const STARSOpndTypePtr
 	return CurrRef;
 }
 
+std::set<DefOrUse, LessDefUse>::const_iterator DefOrUseSet::FindConstRef(const STARSOpndTypePtr &SearchOp) const {
+	set<DefOrUse, LessDefUse>::const_iterator CurrRef;
+	DefOrUse DummyRef(SearchOp);
+	CurrRef = this->Refs.find(DummyRef);
+	return CurrRef;
+
+}
+
 // Insert a new DEF or USE; must be new, insert must succeed else we assert.
 set<DefOrUse, LessDefUse>::iterator DefOrUseSet::InsertRef(DefOrUse Ref) {
 	pair<set<DefOrUse, LessDefUse>::iterator, bool> InsertResult;
diff --git a/src/base/SMPFunction.cpp b/src/base/SMPFunction.cpp
index b2e2186b506cbf8b53d0b88cbe3ba9d1de8b3fae..2a2fa60994d607ed72fca31c70a3f3f32148c19f 100644
--- a/src/base/SMPFunction.cpp
+++ b/src/base/SMPFunction.cpp
@@ -13624,6 +13624,46 @@ int SMPFunction::FindConditionalFollowNode4(const int HeadBlockNum, bool &IfThen
 	bool NoDeadEnds = (!(FTDeadEnd || NFTDeadEnd));
 	bool TooMany = ((FTForwardCount > 1) || (NFTForwardCount > 1));
 	bool NonConvergence = (FTDomFrontierBlockNum != NFTDomFrontierBlockNum);
+
+	if (TooMany) {
+		// Find tight connection (premature merge) between branches of IfThenElse; difficult for our UnlinkPred()
+		//  and EnforceDominanceOnPreds() methods to generalize to handle these, and they are rare, so
+		//  leave them as unstructured. These cause our definition of FTNotDominated and NFTNotDominated
+		//  above (based on Pred count) to be incorrect; we tried to avoid expensive dominance checks using
+		//  the predecessor count and the connection from FT to NFT or NFT to FT ruins that short cut.
+		bool TightError = (FTNotDominated && FTBlock->IsBlockPred(NFTBlock) && (1 < NFTForwardCount));
+		if (!TightError) {
+			TightError = (NFTNotDominated && NFTBlock->IsBlockPred(FTBlock) && (1 < FTForwardCount));
+		}
+		if (!TightError) {
+			// Tight merge might not be tight enough if it passes through a short circuit block set. Check.
+			STARSCFGBlock *FTCFGBlock = this->GetClonedCFGBlockByNum((size_t)FTBlockNum);
+			if (NFTNotDominated && FTCFGBlock->IsExprHeadBlock()) {
+				TightError = ((FTCFGBlock->GetExpr()->GetFallThroughBlockNum() == NFTBlockNum)
+					|| (FTCFGBlock->GetExpr()->GetNonFallThroughBlockNum() == NFTBlockNum));
+			}
+			if (!TightError) {
+				STARSCFGBlock *NFTCFGBlock = this->GetClonedCFGBlockByNum((size_t)NFTBlockNum);
+				if (FTNotDominated && NFTCFGBlock->IsExprHeadBlock()) {
+					TightError = ((NFTCFGBlock->GetExpr()->GetFallThroughBlockNum() == FTBlockNum)
+						|| (NFTCFGBlock->GetExpr()->GetNonFallThroughBlockNum() == FTBlockNum));
+				}
+			}
+		}
+		if (TightError) {
+			FollowBlockNum = SMP_BLOCKNUM_UNINIT;
+			IfThenCase = false;
+			OddIfThenCase = false;
+			IfThenElseCase = true;
+			if (!this->PrintedSPARKUnstructuredMsg) {
+				SMP_msg("ERROR: SPARK: Unstructured due to THEN and ELSE clauses merge prematurely for HeadBlock %d ", HeadBlockNum);
+				this->DumpFuncNameAndAddr();
+				this->PrintedSPARKUnstructuredMsg = true;
+			}
+			return FollowBlockNum;
+		}
+	}
+
 	if ((FTForwardCount == 1) && (NFTForwardCount == 1) && (!NonConvergence)) {
 		FollowBlockNum = FTDomFrontierBlockNum;
 		IfThenCase = false;
@@ -13689,6 +13729,7 @@ int SMPFunction::FindConditionalFollowNode4(const int HeadBlockNum, bool &IfThen
 	bool DominanceError = (IfThenElseError || IfThenError || OddIfThenError);
 	if (DominanceError) {
 		// See if we can salvage any of these errors by checking for straightforward translation patterns.
+
 		if (IfThenElseError && FTDeadEnd && NFTNotDominated && (!FTNotDominated)) {
 			// We can put the FTDeadEnd branch inside an if-then and branch to the NFTBlock/ENDIF.
 			IfThenCase = true;
@@ -13735,6 +13776,40 @@ int SMPFunction::FindConditionalFollowNode4(const int HeadBlockNum, bool &IfThen
 				FollowBlockNum = SMP_BLOCKNUM_UNINIT; // Not cloning
 			}
 		}
+		else if (IfThenElseError && NFTDeadEnd && NFTNotDominated && (!FTNotDominated)) {
+			// NFTNotDominated is only problem; lack of convergence is because of dead end. Clone starting at NFTBlockNum through its dead end.
+			this->ResetTCFGVisitedBlocks();
+			set<int> BlockNumsToClone;
+			bool SafeCloning = this->IsCloningSafe(NFTBlockNum, FollowBlockNum, BlockNumsToClone);
+			if (SafeCloning) {
+				pair<int, int> UnlinkLimitPair(HeadBlockNum, FollowBlockNum);
+				pair<int, pair<int, int> > CloningWorkListItem(NFTBlockNum, UnlinkLimitPair);
+				this->SPARKCloningWorkList.push_back(CloningWorkListItem);
+				SMP_msg("INFO: SPARK: CLONING 9: Cloning from %d to %d would solve DominanceProblem for HeadBlock %d NoDeadEnds %d ", NFTBlockNum, FollowBlockNum, HeadBlockNum, NoDeadEnds);
+				this->DumpFuncNameAndAddr();
+				this->DumpDotCFG();
+			}
+			else {
+				FollowBlockNum = SMP_BLOCKNUM_UNINIT; // Not cloning
+			}
+		}
+		else if (IfThenElseError && FTDeadEnd && FTNotDominated && (!NFTNotDominated)) {
+			// FTNotDominated is only problem; lack of convergence is because of dead end. Clone starting at FTBlockNum through its dead end.
+			this->ResetTCFGVisitedBlocks();
+			set<int> BlockNumsToClone;
+			bool SafeCloning = this->IsCloningSafe(FTBlockNum, FollowBlockNum, BlockNumsToClone);
+			if (SafeCloning) {
+				pair<int, int> UnlinkLimitPair(HeadBlockNum, FollowBlockNum);
+				pair<int, pair<int, int> > CloningWorkListItem(FTBlockNum, UnlinkLimitPair);
+				this->SPARKCloningWorkList.push_back(CloningWorkListItem);
+				SMP_msg("INFO: SPARK: CLONING 10: Cloning from %d to %d would solve DominanceProblem for HeadBlock %d ", FTBlockNum, FollowBlockNum, HeadBlockNum);
+				this->DumpFuncNameAndAddr();
+				this->DumpDotCFG();
+			}
+			else {
+				FollowBlockNum = SMP_BLOCKNUM_UNINIT; // Not cloning
+			}
+		}
 		else if (IfThenElseError && FTNotDominated && NFTNotDominated && (FTDomFrontierBlockNum == NFTDomFrontierBlockNum)) {
 			// Side entrances into both FTBlock and NFTBlock. Cloning can structure it.
 			//  The FTBlock and NFTBlock already have convergence at their DomFrontiers, just have dominance problem.
@@ -13758,6 +13833,9 @@ int SMPFunction::FindConditionalFollowNode4(const int HeadBlockNum, bool &IfThen
 					this->DumpDotCFG();
 				}
 			}
+			if (!SafeCloning) {
+				FollowBlockNum = SMP_BLOCKNUM_UNINIT; // Not cloning
+			}
 		}
 		else if (OddIfThenError) { // NFTNotDominated is the problem; clone starting at NFT
 			this->ResetTCFGVisitedBlocks();
@@ -13959,10 +14037,11 @@ bool SMPFunction::IsCloningSafe(const int StartTCFGBlockNum, const int LimitTCFG
 	// We start our cloning with the manageable cases, so we exclude cloning loops or switch statements.
 	bool TooBig = (this->TCFGBlocks.size() >= (3 * this->RPOBlocks.size())); // limit cloning explosion
 	bool Convergence = (0 < LimitTCFGBlockNum);
+	bool DeadEnd = (SMP_BLOCKNUM_COMMON_RETURN == LimitTCFGBlockNum);
 #if 0
 	bool Safe = ((StartTCFGBlockNum < LimitTCFGBlockNum) && (!CurrTCFGBlock->IsLoopHeaderBlock()) && (!CurrTCFGBlock->HasIndirectJump()) && (!TooBig));
 #else
-	bool Safe = Convergence && ((StartTCFGBlockNum != LimitTCFGBlockNum) && (!CurrTCFGBlock->IsLoopHeaderBlock()) && (!CurrTCFGBlock->HasIndirectJump()) && (!TooBig));
+	bool Safe = (Convergence || DeadEnd) && ((StartTCFGBlockNum != LimitTCFGBlockNum) && (!CurrTCFGBlock->IsLoopHeaderBlock()) && (!CurrTCFGBlock->HasIndirectJump()) && (!TooBig));
 #endif
 	if (Safe && (!CurrTCFGBlock->IsVisited())) {
 		BlockNumsToClone.insert(StartTCFGBlockNum);
@@ -14044,7 +14123,13 @@ void SMPFunction::MarkBlocksAndClone(const int StartingBlockNum, const int Unlin
 				BlockClone->UnlinkPred(UnlinkBlockNum); // Unlink cloned block from any pred dominated by UnlinkBlockNum
 				// Unlink source block from any predecessor not dominated by UnlinkBlockNum, to eliminate unstructured edge.
 				bool PredErased = StartBlock->EnforceDominanceOnPreds(UnlinkBlockNum, NewBlockNum);
+#if 0
+				if (!PredErased) {
+					SMP_msg("WARNING: SPARK: !PredErased in MarkBlocksAndClone for UnlinkBlockNum %d StartingBlockNum %d ", UnlinkBlockNum, StartingBlockNum);
+				}
+#else
 				assert(PredErased);
+#endif
 
 				// The beginning of the path to clone is where some "side entrance" to some structure occurs.
 				//  That means that entries in the JumpFollowNodesMap could be pointing to the beginning block.
@@ -26236,7 +26321,7 @@ void SMPFunction::EmitSPARKAdaForBlock(int CurrTCFGBlockNum, const int DomTCFGBl
 					}
 				}
 				else if ((FlowType == CALL) || (FlowType == INDIR_CALL)) {
-					if (!LastInst->HasBeenTranslatedToSPARK()) {
+					if (!LastInst->HasBeenTranslatedToSPARK() || LastInst->IsBasicBlockTerminator()) {
 						LastInst->EmitSPARKAda(SPARKBodyFile, false);
 					}
 					if (LastCFType == FALL_THROUGH) {
diff --git a/src/base/SMPInstr.cpp b/src/base/SMPInstr.cpp
index a9c90ca019a5fe2bf63d121c2fb82ec151c20723..f512f8e83f9858ef612895ca8a6197c5433dc392 100644
--- a/src/base/SMPInstr.cpp
+++ b/src/base/SMPInstr.cpp
@@ -1083,7 +1083,7 @@ void SMPInstr::PrintSPARKAdaAddressExpr(const STARSOpndTypePtr &Opnd, FILE *OutF
 } // end of PrintSPARKAdaAddressExpr()
 
 // Print an operator in SPARK-Ada form.
-void PrintSPARKAdaOperator(SMPoperator Oper, string &OutString, bool &PrefixProcCall, bool &PrefixUnary, bool ConstFollows) {
+void PrintSPARKAdaOperator(SMPoperator Oper, string &OutString, bool &PrefixProcCall, bool &PrefixUnary, bool ConstFollows, bool ShortCircuitExpr) {
 	PrefixProcCall = false;
 	PrefixUnary = false;
 
@@ -1115,27 +1115,52 @@ void PrintSPARKAdaOperator(SMPoperator Oper, string &OutString, bool &PrefixProc
 
 		case SMP_U_LEFT_SHIFT: // unsigned left shift
 		case SMP_REVERSE_SHIFT_U: // Shift right operand by bit count in left operand
-			OutString = " Interfaces.Shift_Left";
+			if (ShortCircuitExpr) {
+				OutString = " X86.Shift_Left_Func";
+			}
+			else {
+				OutString = " Interfaces.Shift_Left";
+			}
 			PrefixProcCall = true;
 			break;
 
 		case SMP_U_RIGHT_SHIFT: // unsigned right shift
-			OutString = " Interfaces.Shift_Right";
+			if (ShortCircuitExpr) {
+				OutString = " X86.Shift_Right_Func";
+			}
+			else {
+				OutString = " Interfaces.Shift_Right";
+			}
 			PrefixProcCall = true;
 			break;
 
 		case SMP_S_RIGHT_SHIFT: // signed right shift
-			OutString = " Interfaces.Shift_Right_Arithmetic";
+			if (ShortCircuitExpr) {
+				OutString = " X86.Shift_Right_Arithmetic_Func";
+			}
+			else {
+				OutString = " Interfaces.Shift_Right_Arithmetic";
+			}
 			PrefixProcCall = true;
 			break;
 
 		case SMP_ROTATE_LEFT:
-			OutString = " Interfaces.Rotate_Left";
+			if (ShortCircuitExpr) {
+				OutString = " X86.Rotate_Left_Func";
+			}
+			else {
+				OutString = " Interfaces.Rotate_Left";
+			}
 			PrefixProcCall = true;
 			break;
 
 		case SMP_ROTATE_RIGHT:
-			OutString = " Interfaces.Rotate_Right";
+			if (ShortCircuitExpr) {
+				OutString = " X86.Rotate_Right_Func";
+			}
+			else {
+				OutString = " Interfaces.Rotate_Right";
+			}
 			PrefixProcCall = true;
 			break;
 
@@ -1291,11 +1316,10 @@ void PrintSPARKAdaOperator(SMPoperator Oper, string &OutString, bool &PrefixProc
 			PrefixUnary = true;
 			break;
 
+			// Odd binary operations
 		case SMP_GENERAL_COMPARE: // comparisons of packed data, strings, signed, unsigned depending on control words
-		case SMP_UNARY_NUMERIC_OPERATION:  // miscellaneous; produces NUMERIC result
 		case SMP_BINARY_NUMERIC_OPERATION:  // miscellaneous; produces NUMERIC result
 		case SMP_SYSTEM_OPERATION:   // for instructions such as CPUID, RDTSC, etc.; NUMERIC
-		case SMP_UNARY_FLOATING_ARITHMETIC:  // all the same to our type system; all NUMERIC
 		case SMP_BINARY_FLOATING_ARITHMETIC:  // all the same to our type system; all NUMERIC
 
 		case SMP_SHUFFLE: // Shuffle bytes, words, etc. within destination operation per source mask
@@ -1314,15 +1338,24 @@ void PrintSPARKAdaOperator(SMPoperator Oper, string &OutString, bool &PrefixProc
 		case SMP_MAX_U: // dest := unsigned_max(dest, src)
 		case SMP_MIN_S: // dest := signed_min(dest, src)
 		case SMP_MIN_U: // dest := unsigned_min(dest, src)
-		case SMP_ABSOLUTE_VALUE: // take absolute value
 		case SMP_CREATE_MASK: // Create AND-mask from operand and byte/word/dword position # in immediate
 		case SMP_INTERLEAVE: // extended-precision interleaving of bytes or words or dwords etc.; NUMERIC
 		case SMP_CONCATENATE:     // extended-precision concatenation; NUMERIC
 		case SMP_EXTRACT_ZERO_EXTEND: // Extract sub-reg and zero-extend to reg length
 		case SMP_ENCRYPTION_OPERATION: // encryption or decryption bit manipulation operation
-		case SMP_UNARY_POINTER_OPERATION: 
 		case SMP_SIGNAL:   // signal or raise exception
 		default:
+			SMP_msg("ERROR: SPARK: Cannot translate unknown operator: ");
+			SMP_msg(" %s \n", OperatorText[Oper]);
+			OutString = "X86.StrangeArithmetic";
+			PrefixProcCall = true;
+			break;
+
+			// Odd unary operations
+		case SMP_UNARY_NUMERIC_OPERATION:  // miscellaneous; produces NUMERIC result
+		case SMP_UNARY_FLOATING_ARITHMETIC:  // all the same to our type system; all NUMERIC
+		case SMP_ABSOLUTE_VALUE: // take absolute value
+		case SMP_UNARY_POINTER_OPERATION:
 			SMP_msg("ERROR: SPARK: Cannot translate unknown operator: ");
 			SMP_msg(" %s \n", OperatorText[Oper]);
 			OutString = "ERROR";
@@ -2054,7 +2087,7 @@ void SMPRegTransfer::EmitSPARKAdaForRHS(FILE *OutFile, bool RecursiveCall) const
 		SMP_fprintf(OutFile, "(");
 		SMPoperator CurrOper = RightRT->GetOperator();
 		bool ConstFollows = (!RightRT->HasRightSubTree()) && RightRT->GetConstRightOperandNoNorm()->IsImmedOp();
-		PrintSPARKAdaOperator(CurrOper, OperatorString, OperatorIsProcCall, PrefixUnaryOperator, ConstFollows);
+		PrintSPARKAdaOperator(CurrOper, OperatorString, OperatorIsProcCall, PrefixUnaryOperator, ConstFollows, false);
 		const STARSOpndTypePtr LeftOp = RightRT->GetConstLeftOperandNoNorm();
 		if (!OperatorIsProcCall) {
 			if (!PrefixUnaryOperator) {
@@ -2152,7 +2185,7 @@ void SMPRegTransfer::EmitSPARKAda(FILE *OutFile) {
 			if (!SubregWrite) {
 				// Print := operator unless we are assigning with a procedure call.
 				string OutString;
-				PrintSPARKAdaOperator(CurrOper, OutString, OperatorIsProcCall, PrefixUnaryOperator, false);
+				PrintSPARKAdaOperator(CurrOper, OutString, OperatorIsProcCall, PrefixUnaryOperator, false, false);
 				assert(!OperatorIsProcCall);
 				assert(!PrefixUnaryOperator);
 				SMP_fprintf(OutFile, "%s", OutString.c_str());
@@ -2837,7 +2870,7 @@ void STARSExpression::EmitSPARKAda(FILE *OutputFile, bool ProcessingLoop, bool O
 	}
 
 	if (SMP_ASSIGN != CurrOperator) {
-		PrintSPARKAdaOperator(CurrOperator, OperatorString, PrefixProcCall, UnaryPrefix, ConstFollows);
+		PrintSPARKAdaOperator(CurrOperator, OperatorString, PrefixProcCall, UnaryPrefix, ConstFollows, false);
 		if (PrefixProcCall) { // operator comes first, as a procedure call
 			SMP_fprintf(OutputFile, "%s(", OperatorString.c_str());
 		}
@@ -2964,7 +2997,7 @@ void STARSExpression::EmitSPARKAdaString(std::string &OutString, bool Processing
 	}
 
 	if (SMP_ASSIGN != CurrOperator) {
-		PrintSPARKAdaOperator(CurrOperator, OperatorString, PrefixProcCall, UnaryPrefix, ConstFollows);
+		PrintSPARKAdaOperator(CurrOperator, OperatorString, PrefixProcCall, UnaryPrefix, ConstFollows, false);
 		if (PrefixProcCall) { // operator comes first, as a procedure call
 			OutString.append(OperatorString);
 			OutString.append("(");
@@ -6278,7 +6311,7 @@ void SMPInstr::MDEmitSPARKAdaArithmeticSetsCondCodes(FILE *OutFile) {
 		} // end for all LiveFlagRegs set members
 	}
 
-	PrintSPARKAdaOperator(CurrOper, OperatorString, PrefixProcCall, PrefixUnary, ConstFollows);
+	PrintSPARKAdaOperator(CurrOper, OperatorString, PrefixProcCall, PrefixUnary, ConstFollows, false);
 
 	if (!ProcCallHandlesCondCodes) {
 		bool Subtraction = OperatorString == " - ";
@@ -7379,7 +7412,7 @@ void SMPInstr::EmitSPARKAda(FILE *OutFile, const bool DisAsmOnly) {
 
 	case HALT:
 		break;
-	}
+	} // end switch on flow type
 
 	if (PrintOperands) {
 		int BlockNum = this->GetBlock()->GetNumber();
@@ -9405,11 +9438,12 @@ void SMPInstr::Analyze(void) {
 	this->MDFixupIDAProOperandList();
 
 	// See if instruction is an ASM idiom for clearing a register.
-	if ((STARS_NN_xor == opcode) || (STARS_NN_lea == opcode) || (STARS_NN_pxor == opcode)) {
+	bool XorOpcode = ((STARS_NN_xor == opcode) || (STARS_NN_xorps == opcode) || (STARS_NN_pxor == opcode) || (STARS_NN_xorpd == opcode));
+	if (XorOpcode || (STARS_NN_lea == opcode)) {
 		STARSOpndTypePtr FirstOpnd = this->STARSInstPtr->GetOpnd(0);
 		STARSOpndTypePtr SecondOpnd = this->STARSInstPtr->GetOpnd(1);
 		if (!(FirstOpnd->IsMemOp() || FirstOpnd->IsNearPointer() || FirstOpnd->IsFarPointer())) {
-			if ((STARS_NN_xor == opcode) || (STARS_NN_pxor == opcode)) {
+			if (XorOpcode) {
 				// Check for xor of reg with itself
 				// NOTE: We code with IsEqOp() instead of MatchesReg() because we want to include
 				//  odd reg types like xmm, ymm, mmx, etc.
@@ -19207,8 +19241,7 @@ bool SMPInstr::BuildBinaryRTL(SMPoperator BinaryOp, bool HiddenFPStackOp) {
 		STARSOpndTypePtr TempOp = this->STARSInstPtr->GetOpnd(OpNum);
 		if (nullptr == TempOp) // finished processing operands
 			break;
-		if ((this->STARSInstPtr->IsDefOpnd(OpNum))
-			|| (SrcIsReallyDest && (0 == OpNum))) { // DEF
+		if ((this->STARSInstPtr->IsDefOpnd(OpNum)) || (SrcIsReallyDest && (0 == OpNum))) { // DEF
 			if (!DestFound && MDKnownOperandType(TempOp)) {
 				// See comments just below for floating point sources. FP stores
 				//  are analogous to FP loads.
diff --git a/src/drivers/idapro/SMPStaticAnalyzer.cpp b/src/drivers/idapro/SMPStaticAnalyzer.cpp
index e19a70fd03df38a13afe9054d30c74eaebdb44af..258279fa2c6868ce43672da3184109e93e9c24d5 100644
--- a/src/drivers/idapro/SMPStaticAnalyzer.cpp
+++ b/src/drivers/idapro/SMPStaticAnalyzer.cpp
@@ -663,7 +663,7 @@ bool IDAP_run(size_t arg) {
 	return true;
 #endif
 	}
-	catch (std::bad_alloc) {
+	catch (const std::bad_alloc &) {
 		SMP_msg("FATAL ERROR: Memory exhausted.\n");
 		if (nullptr != InfoAnnotFile) {
 			SMP_fprintf(InfoAnnotFile, "   8000000      2 ERROR MEMORYEXHAUSTED\n");