diff --git a/boost_tests/CMakeLists.txt b/boost_tests/CMakeLists.txt
index 59ef49eeb..9417f99e7 100644
--- a/boost_tests/CMakeLists.txt
+++ b/boost_tests/CMakeLists.txt
@@ -11,6 +11,7 @@ add_executable (BinaryPrinterTests BinaryPrinterTests.cpp)
 add_executable (XMLPrinterTests XMLPrinterTests.cpp)
 add_executable (PQLParserTests PQLParserTests.cpp)
 add_executable (PredicateCheckerTests PredicateCheckerTests.cpp)
+add_executable (PushNegationTests PushNegationTests.cpp)
 add_executable (reachability reachability_test.cpp)
 add_executable (ltl ltl_test.cpp)
 add_executable (hyper_ltl hyper_ltl_test.cpp)
@@ -23,6 +24,7 @@ target_link_libraries(BinaryPrinterTests PUBLIC ${Boost_LIBRARIES} -Wl,-Bstatic
 target_link_libraries(XMLPrinterTests    PUBLIC ${Boost_LIBRARIES} -Wl,-Bstatic verifypn -Wl,-Bdynamic)
 target_link_libraries(PQLParserTests     PUBLIC ${Boost_LIBRARIES} -Wl,-Bstatic verifypn -Wl,-Bdynamic)
 target_link_libraries(PredicateCheckerTests     PUBLIC ${Boost_LIBRARIES} -Wl,-Bstatic verifypn -Wl,-Bdynamic)
+target_link_libraries(PushNegationTests  PUBLIC ${Boost_LIBRARIES} -Wl,-Bstatic verifypn -Wl,-Bdynamic)
 target_link_libraries(reachability PUBLIC ${Boost_LIBRARIES} -Wl,-Bstatic verifypn -Wl,-Bdynamic)
 target_link_libraries(ltl PUBLIC ${Boost_LIBRARIES} -Wl,-Bstatic verifypn -Wl,-Bdynamic)
 target_link_libraries(hyper_ltl PUBLIC ${Boost_LIBRARIES} -Wl,-Bstatic verifypn -Wl,-Bdynamic)
@@ -35,6 +37,7 @@ add_test(NAME BinaryPrinterTests COMMAND BinaryPrinterTests)
 add_test(NAME XMLPrinterTests COMMAND XMLPrinterTests)
 add_test(NAME PQLParserTests COMMAND PQLParserTests)
 add_test(NAME PredicateCheckerTests COMMAND PredicateCheckerTests)
+add_test(NAME PushNegationTests COMMAND PushNegationTests)
 add_test(NAME reachability COMMAND reachability)
 add_test(NAME ltl COMMAND ltl)
 add_test(NAME hyper_ltl COMMAND hyper_ltl)
diff --git a/boost_tests/PushNegationTests.cpp b/boost_tests/PushNegationTests.cpp
index 0053ef708..e88d274b7 100644
--- a/boost_tests/PushNegationTests.cpp
+++ b/boost_tests/PushNegationTests.cpp
@@ -7,9 +7,12 @@
 
 using namespace PetriEngine::PQL;
 
+inline std::shared_ptr<IdentifierExpr> make_id(const std::string& name) {
+    return std::make_shared<IdentifierExpr>(std::make_shared<const std::string>(name));
+}
 
 BOOST_AUTO_TEST_CASE(not_less_than_literal_and_identifier) {
-    auto identifier = std::make_shared<IdentifierExpr>("a");
+    auto identifier = make_id("a");
     auto literal = std::make_shared<LiteralExpr>(1);
     auto condition = std::make_shared<NotCondition>(
             std::make_shared<LessThanCondition>(
@@ -30,35 +33,60 @@ BOOST_AUTO_TEST_CASE(not_less_than_literal_and_identifier) {
                           "Less than operands should be swapped");
 }
 
-//BOOST_AUTO_TEST_CASE(AirplaneLD_PT_0050_3) {
-//    auto cond = std::make_shared<NotCondition>(std::make_shared<NotCondition>(
-//            std::make_shared<EGCondition>(
-//                    std::make_shared<AFCondition>(
-//                            std::make_shared<NotCondition>(
-//                                    std::make_shared<ECondition>(
-//                                            std::make_shared<UntilCondition>(
-//                                                    std::make_shared<LessThanOrEqualCondition>(
-//                                                            std::make_shared<PlusExpr>(std::vector<Expr_ptr>{
-//                                                                    std::make_shared<IdentifierExpr>(
-//                                                                            "P3"),
-//                                                                    std::make_shared<IdentifierExpr>(
-//                                                                            "stp5")
-//                                                            }),
-//                                                            std::make_shared<LiteralExpr>(12)
-//                                                    ),
-//                                                    std::make_shared<LessThanOrEqualCondition>(
-//                                                            std::make_shared<PlusExpr>(std::vector<Expr_ptr>{
-//                                                                    std::make_shared<IdentifierExpr>(
-//                                                                            "SpeedPossibleVal_38"),
-//                                                                    std::make_shared<IdentifierExpr>(
-//                                                                            "SpeedPossibleVal_26")
-//                                                            }),
-//                                                            std::make_shared<LiteralExpr>(35)
-//                                                    )
-//                                            )
-//                                    )
-//                            )
-//                    )
-//            )
-//    ));
-//}
+// Regression test for wrong answer in bug #2156598: (P0 - P1) - P2 == 0 must not be rewritten to (P0 - P1) - P2 <= 0, since the subtraction can be negative.
+BOOST_AUTO_TEST_CASE(equal_zero_with_subtraction_is_not_rewritten) {
+    auto subtraction = std::make_shared<SubtractExpr>(std::vector<Expr_ptr>{
+            std::make_shared<SubtractExpr>(std::vector<Expr_ptr>{
+                    make_id("P0"),
+                    make_id("P1")
+            }),
+            make_id("P2")
+    });
+    auto condition = std::make_shared<EqualCondition>(
+            subtraction,
+            std::make_shared<LiteralExpr>(0)
+    );
+    auto stats = negstat_t();
+
+    auto res = pushNegation(condition, stats, EvaluationContext(), false, false, false);
+
+    BOOST_REQUIRE_MESSAGE(std::dynamic_pointer_cast<EqualCondition>(res) != nullptr,
+                          "Equality with possibly negative expression should stay an EqualCondition");
+}
+
+BOOST_AUTO_TEST_CASE(not_equal_zero_with_subtraction_is_not_rewritten) {
+    auto subtraction = std::make_shared<SubtractExpr>(std::vector<Expr_ptr>{
+            make_id("P0"),
+            make_id("P1")
+    });
+    auto condition = std::make_shared<NotCondition>(
+            std::make_shared<EqualCondition>(
+                    subtraction,
+                    std::make_shared<LiteralExpr>(0)
+            )
+    );
+    auto stats = negstat_t();
+
+    auto res = pushNegation(condition, stats, EvaluationContext(), false, false, false);
+
+    BOOST_REQUIRE_MESSAGE(std::dynamic_pointer_cast<NotEqualCondition>(res) != nullptr,
+                          "Negated equality with possibly negative expression should become NotEqualCondition");
+}
+
+// Keep rewrite for non-negative expressions: P0 + P1 == 0  ->  P0 + P1 <= 0
+BOOST_AUTO_TEST_CASE(equal_zero_with_plus_is_rewritten_to_leq) {
+    auto sum = std::make_shared<PlusExpr>(std::vector<Expr_ptr>{
+            make_id("P0"),
+            make_id("P1")
+    });
+    auto condition = std::make_shared<EqualCondition>(
+            sum,
+            std::make_shared<LiteralExpr>(0)
+    );
+    auto stats = negstat_t();
+
+    auto res = pushNegation(condition, stats, EvaluationContext(), false, false, false);
+
+    BOOST_REQUIRE_MESSAGE(std::dynamic_pointer_cast<LessThanOrEqualCondition>(res) != nullptr,
+                          "Equality with non-negative expression should be rewritten to LessThanOrEqual");
+}