diff --git a/src/base/SMPBasicBlock.cpp b/src/base/SMPBasicBlock.cpp
index 225b8c5cc650e962259df7158fc54e02c4ebe716..60930dd750327f2be595dbdec4ac23ea46a5cb80 100644
--- a/src/base/SMPBasicBlock.cpp
+++ b/src/base/SMPBasicBlock.cpp
@@ -719,6 +719,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 +776,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,8 +913,8 @@ 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;
@@ -8127,7 +8159,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 +8193,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;