diff --git a/SMTPlan/src/EncoderHappening.cpp b/SMTPlan/src/EncoderHappening.cpp
index 61c97c0..fb17bec 100644
--- a/SMTPlan/src/EncoderHappening.cpp
+++ b/SMTPlan/src/EncoderHappening.cpp
@@ -1352,10 +1352,10 @@ namespace SMTPlan {
 		s->getLHS()->visit(this);
 		s->getRHS()->visit(this);
 
-		z3::expr lhs = enc_expression_stack.back();
-		enc_expression_stack.pop_back();
 		z3::expr rhs = enc_expression_stack.back();
 		enc_expression_stack.pop_back();
+		z3::expr lhs = enc_expression_stack.back();
+		enc_expression_stack.pop_back();
 		enc_expression_stack.push_back(lhs + rhs);
 	}
 
@@ -1364,10 +1364,10 @@ namespace SMTPlan {
 		s->getLHS()->visit(this);
 		s->getRHS()->visit(this);
 
-		z3::expr lhs = enc_expression_stack.back();
-		enc_expression_stack.pop_back();
 		z3::expr rhs = enc_expression_stack.back();
 		enc_expression_stack.pop_back();
+		z3::expr lhs = enc_expression_stack.back();
+		enc_expression_stack.pop_back();
 		enc_expression_stack.push_back(lhs - rhs);
 	}
 
@@ -1376,10 +1376,10 @@ namespace SMTPlan {
 		s->getLHS()->visit(this);
 		s->getRHS()->visit(this);
 
-		z3::expr lhs = enc_expression_stack.back();
-		enc_expression_stack.pop_back();
 		z3::expr rhs = enc_expression_stack.back();
 		enc_expression_stack.pop_back();
+		z3::expr lhs = enc_expression_stack.back();
+		enc_expression_stack.pop_back();
 		enc_expression_stack.push_back(lhs * rhs);
 	}