From 8b3420edc1d98cfbc15238ec0d6992e4637a5073 Mon Sep 17 00:00:00 2001
From: Jendrik Seipp <jendrik.seipp@liu.se>
Date: Sat, 26 Aug 2023 08:01:28 +0200
Subject: [PATCH 1/2] Only print flawed state if we actually use it (in debug
 mode).

---
 src/search/cegar/flaw.h         |  2 +-
 src/search/cegar/flaw_search.cc | 10 +++++-----
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/search/cegar/flaw.h b/src/search/cegar/flaw.h
index 07cfa70e7..420ae3b58 100644
--- a/src/search/cegar/flaw.h
+++ b/src/search/cegar/flaw.h
@@ -38,7 +38,7 @@ struct FlawedState {
     }
 
     friend std::ostream &operator<<(std::ostream &os, const FlawedState &s) {
-        return os << "Flawed abstract state: id=" << s.abs_id << ", h=" << s.h
+        return os << "id=" << s.abs_id << ", h=" << s.h
                   << ", states=" << s.concrete_states.size();
     }
 
diff --git a/src/search/cegar/flaw_search.cc b/src/search/cegar/flaw_search.cc
index 8e2653b3e..d274a8603 100644
--- a/src/search/cegar/flaw_search.cc
+++ b/src/search/cegar/flaw_search.cc
@@ -476,7 +476,7 @@ unique_ptr<Split>
 FlawSearch::get_min_h_batch_split(const utils::CountdownTimer &cegar_timer) {
     assert(pick_flawed_abstract_state == PickFlawedAbstractState::BATCH_MIN_H);
     if (last_refined_flawed_state != FlawedState::no_state) {
-        // Handle flaws of the last refined abstract state.
+        // Recycle flaws of the last refined abstract state.
         Cost old_h = last_refined_flawed_state.h;
         for (const StateID &state_id : last_refined_flawed_state.concrete_states) {
             State state = state_registry->lookup_state(state_id);
@@ -498,10 +498,6 @@ FlawSearch::get_min_h_batch_split(const utils::CountdownTimer &cegar_timer) {
         }
     }
 
-    if (log.is_at_least_debug()) {
-        log << "Use flawed state: " << flawed_state << " with h=" << flawed_state.h << endl;
-    }
-
     // Memory padding
     if (search_status == TIMEOUT)
         return nullptr;
@@ -510,6 +506,10 @@ FlawSearch::get_min_h_batch_split(const utils::CountdownTimer &cegar_timer) {
         // There are flaws to refine.
         assert(flawed_state != FlawedState::no_state);
 
+        if (log.is_at_least_debug()) {
+            log << "Use flawed state: " << flawed_state << endl;
+        }
+
         unique_ptr<Split> split;
         split = create_split(flawed_state.concrete_states, flawed_state.abs_id);
 

From 6e1f1c5fc4b79302f47665df7b3d9f836694f0c4 Mon Sep 17 00:00:00 2001
From: Jendrik Seipp <jendrik.seipp@liu.se>
Date: Mon, 28 Aug 2023 15:21:10 +0200
Subject: [PATCH 2/2] Abort separating goal- from non-goal states when resource
 limits are hit.

---
 src/search/cegar/cegar.cc | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/search/cegar/cegar.cc b/src/search/cegar/cegar.cc
index 88303eeb2..890c91cec 100644
--- a/src/search/cegar/cegar.cc
+++ b/src/search/cegar/cegar.cc
@@ -158,6 +158,9 @@ void CEGAR::refinement_loop() {
         assert(abstraction->get_num_states() == 1);
         const AbstractState *current = &abstraction->get_initial_state();
         for (FactProxy goal : task_proxy.get_goals()) {
+            if (!may_keep_refining()) {
+                break;
+            }
             FactPair fact = goal.get_pair();
             auto pair = abstraction->refine(*current, fact.var, {fact.value});
             current = &abstraction->get_state(pair.second);