From 9e4627c4669fdaeff75cf7e1e3b5391195001806 Mon Sep 17 00:00:00 2001 From: Nathan Hunt Date: Wed, 15 Feb 2023 13:45:24 -0500 Subject: [PATCH] Fix LHS vs RHS in arithmetic expressions. Fixes #19. `visit_div_expression` already had the correct method of popping the RHS first then the LHS. However, plus, minus and mul all switched the order and called the first thing popped from the stack the LHS. For plus and mul, this doesn't affect the correctness, but it lead to minus being interpreted backwards (see the linked issue). I think this should fix that issue, but I'm not familiar with the code base, so please let me know if there are other places this change would need to be made too. --- SMTPlan/src/EncoderHappening.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) 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); }