From d3dee19525c7026a8787eb6808f7ff18b60d4aaa Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 29 Nov 2025 18:57:16 +0100
Subject: [PATCH] Catch out-of-memory exceptions during propositional reduction

We already caught out-of-memory exceptions in some places in the solver
back-ends, but not at the more global level of various propositional
reduction steps.

Fixes: #727
---
 src/goto-checker/bmc_util.cpp         | 22 +++++++--
 src/solvers/prop/prop_conv_solver.cpp | 66 ++++++++++++++++-----------
 2 files changed, 56 insertions(+), 32 deletions(-)

diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp
index d7ea8ada8c4..5bb3d9ce459 100644
--- a/src/goto-checker/bmc_util.cpp
+++ b/src/goto-checker/bmc_util.cpp
@@ -347,11 +347,23 @@ std::chrono::duration<double> prepare_property_decider(
     << property_decider.get_decision_procedure().decision_procedure_text()
     << messaget::eom;
 
-  convert_symex_target_equation(
-    equation, property_decider.get_decision_procedure(), ui_message_handler);
-  property_decider.update_properties_goals_from_symex_target_equation(
-    properties);
-  property_decider.convert_goals();
+  try
+  {
+    convert_symex_target_equation(
+      equation, property_decider.get_decision_procedure(), ui_message_handler);
+    property_decider.update_properties_goals_from_symex_target_equation(
+      properties);
+    property_decider.convert_goals();
+  }
+  catch(const std::bad_alloc &)
+  {
+    log.error() << "Solver ran out of memory during propositional reduction."
+                << messaget::eom;
+    log.error()
+      << "Try reducing the problem size or increasing available memory."
+      << messaget::eom;
+    throw;
+  }
 
   auto solver_stop = std::chrono::steady_clock::now();
   return std::chrono::duration<double>(solver_stop - solver_start);
diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp
index a8385c08272..505e450a150 100644
--- a/src/solvers/prop/prop_conv_solver.cpp
+++ b/src/solvers/prop/prop_conv_solver.cpp
@@ -443,44 +443,56 @@ void prop_conv_solvert::finish_eager_conversion()
 decision_proceduret::resultt
 prop_conv_solvert::dec_solve(const exprt &assumption)
 {
-  // post-processing isn't incremental yet
-  if(!post_processing_done)
+  try
   {
-    const auto post_process_start = std::chrono::steady_clock::now();
+    // post-processing isn't incremental yet
+    if(!post_processing_done)
+    {
+      const auto post_process_start = std::chrono::steady_clock::now();
 
-    log.progress() << "Post-processing" << messaget::eom;
-    finish_eager_conversion();
-    post_processing_done = true;
+      log.progress() << "Post-processing" << messaget::eom;
+      finish_eager_conversion();
+      post_processing_done = true;
 
-    const auto post_process_stop = std::chrono::steady_clock::now();
-    std::chrono::duration<double> post_process_runtime =
-      std::chrono::duration<double>(post_process_stop - post_process_start);
-    log.statistics() << "Runtime Post-process: " << post_process_runtime.count()
-                     << "s" << messaget::eom;
-  }
+      const auto post_process_stop = std::chrono::steady_clock::now();
+      std::chrono::duration<double> post_process_runtime =
+        std::chrono::duration<double>(post_process_stop - post_process_start);
+      log.statistics() << "Runtime Post-process: "
+                       << post_process_runtime.count() << "s" << messaget::eom;
+    }
 
-  log.progress() << "Solving with " << prop.solver_text() << messaget::eom;
+    log.progress() << "Solving with " << prop.solver_text() << messaget::eom;
 
-  if(assumption.is_nil())
-    push();
-  else
-    push({assumption});
+    if(assumption.is_nil())
+      push();
+    else
+      push({assumption});
 
-  auto prop_result = prop.prop_solve(assumption_stack);
+    auto prop_result = prop.prop_solve(assumption_stack);
 
-  pop();
+    pop();
 
-  switch(prop_result)
+    switch(prop_result)
+    {
+    case propt::resultt::P_SATISFIABLE:
+      return resultt::D_SATISFIABLE;
+    case propt::resultt::P_UNSATISFIABLE:
+      return resultt::D_UNSATISFIABLE;
+    case propt::resultt::P_ERROR:
+      return resultt::D_ERROR;
+    }
+
+    UNREACHABLE;
+  }
+  catch(const std::bad_alloc &)
   {
-  case propt::resultt::P_SATISFIABLE:
-    return resultt::D_SATISFIABLE;
-  case propt::resultt::P_UNSATISFIABLE:
-    return resultt::D_UNSATISFIABLE;
-  case propt::resultt::P_ERROR:
+    log.error() << "Solver ran out of memory during propositional reduction."
+                << messaget::eom;
+    log.error()
+      << "Try reducing the problem size or increasing available memory."
+      << messaget::eom;
     return resultt::D_ERROR;
   }
-
-  UNREACHABLE;
 }
 
 exprt prop_conv_solvert::get(const exprt &expr) const