From f30263f87b69c635c86b86087cf2056812b8394b Mon Sep 17 00:00:00 2001
From: Simon Sorg <simon.sorg@student.hpi.de>
Date: Sat, 12 Apr 2025 11:43:45 +0100
Subject: [PATCH 1/3] fix: use kill_tactic of graph rather than node for
 recursive calls

---
 src/graph/graph.h | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/graph/graph.h b/src/graph/graph.h
index c634ab4..7fbced8 100644
--- a/src/graph/graph.h
+++ b/src/graph/graph.h
@@ -1537,7 +1537,11 @@ namespace htps {
                 if (node.is_bad()) {
                     for (const auto &[parent_th, tactic_id]: ancestors.get_ancestors(th)) {
                         if (!parent_th.empty()) {
-                            nodes.at(parent_th)->kill_tactic(tactic_id);
+                            if (!nodes.contains(parent_th)) {
+                                std::string msg = "Parent node not found: " + parent_th;
+                                throw std::runtime_error(msg);
+                            }
+                            kill_tactic(nodes.at(parent_th), tactic_id);
                         }
                     }
                     continue;

From 8fa560d0bdd331f2cf254441e4bd88eb2f0c600c Mon Sep 17 00:00:00 2001
From: Simon Sorg <simon.sorg@student.hpi.de>
Date: Sat, 12 Apr 2025 11:44:06 +0100
Subject: [PATCH 2/3] fix: store ancestor set before iterating

---
 src/graph/graph.h | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/graph/graph.h b/src/graph/graph.h
index 7fbced8..43c3c1e 100644
--- a/src/graph/graph.h
+++ b/src/graph/graph.h
@@ -1535,7 +1535,8 @@ namespace htps {
                 std::shared_ptr<T> node_ptr = std::make_shared<T>(node);
                 nodes.set(th, node_ptr);
                 if (node.is_bad()) {
-                    for (const auto &[parent_th, tactic_id]: ancestors.get_ancestors(th)) {
+                    const AncestorSet anc = ancestors.get_ancestors(th);
+                    for (const auto &[parent_th, tactic_id]: anc) {
                         if (!parent_th.empty()) {
                             if (!nodes.contains(parent_th)) {
                                 std::string msg = "Parent node not found: " + parent_th;

From 05fb48910f137ed54b60e12ec0dde8e4c1d59ae9 Mon Sep 17 00:00:00 2001
From: Simon Sorg <simon.sorg@student.hpi.de>
Date: Sat, 12 Apr 2025 12:10:44 +0100
Subject: [PATCH 3/3] test: propagate killed tactic through two theorems

---
 tests/htps_tests.cpp | 59 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 59 insertions(+)

diff --git a/tests/htps_tests.cpp b/tests/htps_tests.cpp
index d9d087d..f5298cb 100644
--- a/tests/htps_tests.cpp
+++ b/tests/htps_tests.cpp
@@ -920,6 +920,65 @@ TEST_F(HTPSTest, TestAddToKilled) {
     EXPECT_TRUE(proof_samples_tactics.empty());
 }
 
+/* If the last child of a node is killed, the corresponding parent should be killed too.
+ */
+TEST_F(HTPSTest, TestKilledRecursively) {
+    htps_instance->theorems_to_expand();
+
+    TheoremPointer child1 = static_pointer_cast<htps::theorem>(std::make_shared<DummyTheorem>("B1"));
+    std::vector<std::shared_ptr<htps::env_effect>> effects;
+    auto effect = std::make_shared<htps::env_effect>();
+    effect->goal = root;
+    effect->tac = dummyTac;
+    effect->children = {child1};
+    effects.push_back(effect);
+
+    std::vector<std::shared_ptr<htps::tactic>> tactics = {dummyTac};
+    std::vector<std::vector<htps::TheoremPointer>> childrenForTactic = {{child1}};
+    std::vector<double> priors = {1.0};
+    std::vector<size_t> envDurations = {1};
+
+    htps::env_expansion expansion(root, 1, 1, envDurations, effects, 0.0, tactics, childrenForTactic, priors);
+    std::vector<std::shared_ptr<htps::env_expansion>> expansions = {std::make_shared<htps::env_expansion>(expansion)};
+
+    htps_instance->expand_and_backup(expansions);
+    expansions.clear();
+
+    auto theorems = htps_instance->theorems_to_expand();
+    EXPECT_TRUE(theorems[0] == child1 && theorems.size() == 1);
+
+    TheoremPointer child2 = static_pointer_cast<htps::theorem>(std::make_shared<DummyTheorem>("B2"));
+    effects.clear();
+    effect = std::make_shared<htps::env_effect>();
+    effect->goal = root;
+    effect->tac = dummyTac2;
+    effect->children = {child2};
+    effects.push_back(effect);
+
+    tactics = {dummyTac2};
+    childrenForTactic = {{child2}};
+    priors = {1.0};
+    envDurations = {1};
+    expansion = {child1, 1, 1, envDurations, effects, 0.0, tactics, childrenForTactic, priors};
+    expansions = {std::make_shared<htps::env_expansion>(expansion)};
+    htps_instance->expand_and_backup(expansions);
+    expansions.clear();
+
+    theorems = htps_instance->theorems_to_expand();
+    EXPECT_TRUE(theorems[0] == child2 && theorems.size() == 1);
+
+    envDurations = {1, 1, 1};
+    std::string error = "This is broken!";
+    expansion = {child2, 1, 1, envDurations, error};
+    expansions = {std::make_shared<htps::env_expansion>(expansion)};
+    htps_instance->expand_and_backup(expansions);
+
+    htps_instance->theorems_to_expand();
+    EXPECT_TRUE(htps_instance->is_done());
+    EXPECT_FALSE(htps_instance->is_proven());
+    EXPECT_TRUE(htps_instance->dead_root());
+}
+
 /* Two tactics leading to the same children from the same starting node.
  */
 TEST_F(HTPSTest, TestMultipleSame) {