Repository: chrjabs/rustsat (language: python)

Issue:
"fatal runtime error: Rust cannot catch foreign exceptions"
Hi, in some experiments with CaDiCaL and Minisat I managed to get this error message (on Intel-Linux):

> fatal runtime error: Rust cannot catch foreign exceptions

Some of these errors came after ≈ 40 hours of computation, so it won't be quick to reproduce, but I'm wondering if it is possible that memory allocation errors in the solver library might be reported like this? Or is it known that the solver running out of memory will be reported in a different way and this has to be something else?
"fatal runtime error: Rust cannot catch foreign exceptions"
Hi, in some experiments with CaDiCaL and Minisat I managed to get this error message (on Intel-Linux):

> fatal runtime error: Rust cannot catch foreign exceptions

Some of these errors came after ≈ 40 hours of computation, so it won't be quick to reproduce, but I'm wondering if it is possible that memory allocation errors in the solver library might be reported like this? Or is it known that the solver running out of memory will be reported in a different way and this has to be something else?


Discussion / hints:
Yes, this is most likely a memory allocation error in one of the C++ libraries. At least in this case I have seen the same error message before.

Longer term one could put some work into catching the C++ memory exceptions in the C-wrappers and then passing some error message to Rust, so that a nicer error can be returned. This would enable doing some cleanup tasks in Rust when this happens.
One suggestion if this is fixed, based on my past experience interfacing with minisat (and many solvers are inspired by, or derived from, minisat).

It's not that hard to catch this, minisat-derived solvers throw an 'OutOfMemoryException' (which isn't a C++ standard thing).

If that happens however, from my past experience there isn't much more you can do than just `panic!` (I abort()ed in C++) with a more helpful error message, as the solver can be left in a weird state where it won't clean itself up properly if you destroy it (I don't remember all the details, but I did hit this, and obviously it's a hard thing to write proper tests for.).

When minisat catches an OutOfMemoryException minisat doesn't try to do any cleanup, it just prints "INDETERMINATE" and exits.

One thing I will mention (again, from past experience), quite a few solvers use 32-bit counts for sizes, so you might find they "run out of memory" while you still have lots of memory. I don't know if some of the more modern solvers like kissat remove this limitation (it's in minisat and glucose)
I'd be very happy with a panic, as long as the error message gives some hint that it is related to memory allocation.
Alright, that is a pretty solid idea now. I'll see whether I can give this a go in the near future.
Yes, this is most likely a memory allocation error in one of the C++ libraries. At least in this case I have seen the same error message before.

Longer term one could put some work into catching the C++ memory exceptions in the C-wrappers and then passing some error message to Rust, so that a nicer error can be returned. This would enable doing some cleanup tasks in Rust when this happens.
One suggestion if this is fixed, based on my past experience interfacing with minisat (and many solvers are inspired by, or derived from, minisat).

It's not that hard to catch this, minisat-derived solvers throw an 'OutOfMemoryException' (which isn't a C++ standard thing).

If that happens however, from my past experience there isn't much more you can do than just `panic!` (I abort()ed in C++) with a more helpful error message, as the solver can be left in a weird state where it won't clean itself up properly if you destroy it (I don't remember all the details, but I did hit this, and obviously it's a hard thing to write proper tests for.).

When minisat catches an OutOfMemoryException minisat doesn't try to do any cleanup, it just prints "INDETERMINATE" and exits.

One thing I will mention (again, from past experience), quite a few solvers use 32-bit counts for sizes, so you might find they "run out of memory" while you still have lots of memory. I don't know if some of the more modern solvers like kissat remove this limitation (it's in minisat and glucose)
I'd be very happy with a panic, as long as the error message gives some hint that it is related to memory allocation.
Alright, that is a pretty solid idea now. I'll see whether I can give this a go in the near future.

Fix patch:
diff --git a/.github/workflows/capi.yml b/.github/workflows/capi.yml
index 95062a70..a68ca0c8 100644
--- a/.github/workflows/capi.yml
+++ b/.github/workflows/capi.yml
@@ -37,6 +37,8 @@ jobs:
     name: Ensure C-API crate version is in sync
     runs-on: ubuntu-latest
     steps:
+      - name: Checkout sources
+        uses: actions/checkout@v4
       - name: Check
         run: "[ \"$(grep '^version = ' rustsat/Cargo.toml)\" = \"$(grep '^version = ' capi/Cargo.toml)\" ]"
 
diff --git a/.github/workflows/pyapi.yml b/.github/workflows/pyapi.yml
index 3bacde19..2af819a5 100644
--- a/.github/workflows/pyapi.yml
+++ b/.github/workflows/pyapi.yml
@@ -54,6 +54,8 @@ jobs:
     name: Ensure Python API crate version is in sync
     runs-on: ubuntu-latest
     steps:
+      - name: Checkout sources
+        uses: actions/checkout@v4
       - name: Check
         run: "[ \"$(grep '^version = ' rustsat/Cargo.toml)\" = \"$(grep '^version = ' pyapi/Cargo.toml)\" ]"
 
diff --git a/cadical/Cargo.toml b/cadical/Cargo.toml
index 9afb53af..aa1ed892 100644
--- a/cadical/Cargo.toml
+++ b/cadical/Cargo.toml
@@ -53,3 +53,5 @@ chrono = "0.4.31"
 
 [dev-dependencies]
 rustsat-solvertests = { path = "../solvertests" }
+clap = { version = "4.5.4", features = ["derive"] }
+signal-hook = { version = "0.3.17" }
diff --git a/cadical/examples/cadical-cli.rs b/cadical/examples/cadical-cli.rs
new file mode 100644
index 00000000..6db718af
--- /dev/null
+++ b/cadical/examples/cadical-cli.rs
@@ -0,0 +1,129 @@
+//! # CaDiCaL CLI Tool
+//!
+//! A simple CLI wrapper around the CaDiCaL solver Rust interface. This is just an example, if you
+//! want to use CaDiCaL from the CLI, compile the binary from the C++ source directly.
+
+use std::{
+    io,
+    path::{Path, PathBuf},
+    thread,
+};
+
+use anyhow::Context;
+use clap::Parser;
+use rustsat::{
+    instances::{fio::opb, ManageVars, SatInstance},
+    solvers::{Interrupt, InterruptSolver, Solve, SolveStats, SolverResult},
+};
+use rustsat_cadical::CaDiCaL;
+
+enum FileType {
+    Cnf,
+    Opb,
+}
+
+#[derive(Parser)]
+#[command(author, version, about, long_about = None)]
+struct Args {
+    /// The DIMACS CNF input file. Reads from `stdin` if not given.
+    in_path: Option<PathBuf>,
+    /// Parse the input as an OPB file by default
+    #[arg(short, long)]
+    opb: bool,
+}
+
+fn main() -> anyhow::Result<()> {
+    let args = Args::parse();
+
+    let inst: SatInstance = if let Some(in_path) = args.in_path {
+        match determine_file_type(&in_path, args.opb) {
+            FileType::Cnf => SatInstance::from_dimacs_path(in_path)
+                .context("error parsing the input file as CNF")?,
+            FileType::Opb => SatInstance::from_opb_path(in_path, opb::Options::default())
+                .context("error parsing the input file as OPB")?,
+        }
+    } else if args.opb {
+        SatInstance::from_opb(io::BufReader::new(io::stdin()), opb::Options::default())
+            .context("error parsing input as OPB")?
+    } else {
+        SatInstance::from_dimacs(io::BufReader::new(io::stdin()))
+            .context("error parsing input as CNF")?
+    };
+
+    solve::<CaDiCaL>(inst)
+}
+
+fn solve<S: Solve + SolveStats + Interrupt + Default>(inst: SatInstance) -> anyhow::Result<()> {
+    let mut solver = S::default();
+
+    #[cfg(not(target_family = "windows"))]
+    {
+        // Setup signal handling
+        let interrupter = solver.interrupter();
+        let mut signals = signal_hook::iterator::Signals::new([
+            signal_hook::consts::SIGTERM,
+            signal_hook::consts::SIGINT,
+            signal_hook::consts::SIGXCPU,
+            signal_hook::consts::SIGABRT,
+        ])?;
+        // Thread for catching incoming signals
+        thread::spawn(move || {
+            for _ in signals.forever() {
+                interrupter.interrupt();
+            }
+        });
+    }
+
+    let (cnf, vm) = inst.into_cnf();
+    if let Some(max_var) = vm.max_var() {
+        solver.reserve(max_var)?;
+    }
+    solver.add_cnf(cnf)?;
+    match solver.solve() {
+        Err(err) => {
+            println!("s UNKNOWN");
+            return Err(err);
+        }
+        Ok(res) => match res {
+            SolverResult::Sat => {
+                println!("s SATISFIABLE");
+                println!("v {}", solver.full_solution()?);
+            }
+            SolverResult::Unsat => println!("s UNSATISFIABLE"),
+            SolverResult::Interrupted => println!("s UNKNOWN"),
+        },
+    };
+    Ok(())
+}
+
+macro_rules! is_one_of {
+    ($a:expr, $($b:expr),*) => {
+        $( $a == $b || )* false
+    }
+}
+
+fn determine_file_type(in_path: &Path, opb_default: bool) -> FileType {
+    if let Some(ext) = in_path.extension() {
+        let path_without_compr = in_path.with_extension("");
+        let ext = if is_one_of!(ext, "gz", "bz2") {
+            // Strip compression extension
+            match path_without_compr.extension() {
+                Some(ext) => ext,
+                None => return FileType::Cnf, // Fallback default
+            }
+        } else {
+            ext
+        };
+        if "opb" == ext {
+            return FileType::Opb;
+        };
+        if "cnf" == ext {
+            return FileType::Cnf;
+        }
+    };
+    if opb_default {
+        FileType::Opb
+    } else {
+        FileType::Cnf
+    } // Fallback default
+}
diff --git a/cadical/patches/v150.patch b/cadical/patches/v150.patch
index 9d228f7a..22af07d6 100644
--- a/cadical/patches/v150.patch
+++ b/cadical/patches/v150.patch
@@ -1,14 +1,14 @@
-From d153963a145ae94c0f3ce695ec1dc89fe73a9815 Mon Sep 17 00:00:00 2001
+From cc5a76a68bd5f05b0b45c9d335605521228e7d5d Mon Sep 17 00:00:00 2001
 From: Christoph Jabs <christoph.jabs@helsinki.fi>
-Date: Wed, 23 Aug 2023 11:30:43 +0300
+Date: Thu, 18 Apr 2024 15:04:18 +0300
 Subject: [PATCH] extend C api
 
 ---
- src/cadical.hpp  |  6 ++++++
- src/ccadical.cpp | 54 ++++++++++++++++++++++++++++++++++++++++++++++++
- src/ccadical.h   | 17 +++++++++++++++
- src/solver.cpp   | 24 +++++++++++++++++++++
- 4 files changed, 101 insertions(+)
+ src/cadical.hpp  |  6 ++++
+ src/ccadical.cpp | 94 ++++++++++++++++++++++++++++++++++++++++++++++++
+ src/ccadical.h   | 24 +++++++++++++
+ src/solver.cpp   | 24 +++++++++++++
+ 4 files changed, 148 insertions(+)
 
 diff --git a/src/cadical.hpp b/src/cadical.hpp
 index cbe476d..e5e8a9f 100644
@@ -28,10 +28,10 @@ index cbe476d..e5e8a9f 100644
  
    // Enables clausal proof tracing in DRAT format and returns 'true' if
 diff --git a/src/ccadical.cpp b/src/ccadical.cpp
-index e6e7d28..7fabb24 100644
+index e6e7d28..853d11c 100644
 --- a/src/ccadical.cpp
 +++ b/src/ccadical.cpp
-@@ -177,4 +177,58 @@ int ccadical_frozen (CCaDiCaL * ptr, int lit) {
+@@ -177,4 +177,98 @@ int ccadical_frozen (CCaDiCaL * ptr, int lit) {
    return ((Wrapper*) ptr)->solver->frozen (lit);
  }
  
@@ -39,6 +39,41 @@ index e6e7d28..7fabb24 100644
 +
 +// Extending C API (Christoph Jabs)
 +
++int ccadical_add_mem (CCaDiCaL * wrapper, int lit) {
++  try {
++    ((Wrapper*) wrapper)->solver->add (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_assume_mem (CCaDiCaL * wrapper, int lit) {
++  try {
++    ((Wrapper*) wrapper)->solver->assume (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_constrain_mem (CCaDiCaL *wrapper, int lit){
++  try {
++    ((Wrapper*) wrapper)->solver->constrain (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_solve_mem (CCaDiCaL * wrapper) {
++  try {
++    return ((Wrapper*) wrapper)->solver->solve ();
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
 +bool ccadical_configure (CCaDiCaL *ptr, const char *name) {
 +  return ((Wrapper *) ptr)->solver->configure (name);
 +}
@@ -72,8 +107,13 @@ index e6e7d28..7fabb24 100644
 +  return ((Wrapper *) wrapper)->solver->simplify (rounds);
 +}
 +
-+void ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
-+  return ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++int ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
++  try {
++    ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
 +}
 +
 +int64_t ccadical_propagations (CCaDiCaL *wrapper) {
@@ -91,15 +131,22 @@ index e6e7d28..7fabb24 100644
 +/*------------------------------------------------------------------------*/
  }
 diff --git a/src/ccadical.h b/src/ccadical.h
-index 332f842..1a141f4 100644
+index 332f842..db41678 100644
 --- a/src/ccadical.h
 +++ b/src/ccadical.h
-@@ -50,6 +50,23 @@ int ccadical_simplify (CCaDiCaL *);
+@@ -50,6 +50,30 @@ int ccadical_simplify (CCaDiCaL *);
  
  /*------------------------------------------------------------------------*/
  
 +// Extending C API (Christoph Jabs)
 +
++// This value is returned from _solve_mem, _add_mem, _constrain_mem, and _assume_mem
++const int OUT_OF_MEM = 50;
++
++int ccadical_add_mem (CCaDiCaL *, int lit);
++int ccadical_assume_mem (CCaDiCaL *, int lit);
++int ccadical_constrain_mem (CCaDiCaL *, int lit);
++int ccadical_solve_mem (CCaDiCaL *);
 +bool ccadical_configure (CCaDiCaL *, const char *);
 +void ccadical_phase (CCaDiCaL *, int lit);
 +void ccadical_unphase (CCaDiCaL *, int lit);
@@ -108,7 +155,7 @@ index 332f842..1a141f4 100644
 +bool ccadical_limit_ret (CCaDiCaL *, const char *name, int val);
 +int64_t ccadical_redundant (CCaDiCaL *);
 +int ccadical_simplify_rounds (CCaDiCaL *, int rounds);
-+void ccadical_reserve (CCaDiCaL *, int min_max_var);
++int ccadical_reserve (CCaDiCaL *, int min_max_var);
 +int64_t ccadical_propagations (CCaDiCaL *);
 +int64_t ccadical_decisions (CCaDiCaL *);
 +int64_t ccadical_conflicts (CCaDiCaL *);
@@ -154,5 +201,5 @@ index 31b1610..a079861 100644
  
  void Solver::freeze (int lit) {
 -- 
-2.41.0
+2.44.0
 
diff --git a/cadical/patches/v154.patch b/cadical/patches/v154.patch
index 88f6f5a8..099de647 100644
--- a/cadical/patches/v154.patch
+++ b/cadical/patches/v154.patch
@@ -1,14 +1,14 @@
-From 0a29abb1115e1bf09819f27fb3fb2db09f0b6759 Mon Sep 17 00:00:00 2001
+From 3465e6b4145153961fad7d7d7b8e87f2f1992d33 Mon Sep 17 00:00:00 2001
 From: Christoph Jabs <christoph.jabs@helsinki.fi>
-Date: Wed, 23 Aug 2023 11:30:43 +0300
+Date: Thu, 18 Apr 2024 15:05:41 +0300
 Subject: [PATCH] extend C api
 
 ---
- src/cadical.hpp  |  6 +++++
- src/ccadical.cpp | 62 ++++++++++++++++++++++++++++++++++++++++++++++++
- src/ccadical.h   | 19 +++++++++++++++
- src/solver.cpp   | 24 +++++++++++++++++++
- 4 files changed, 111 insertions(+)
+ src/cadical.hpp  |   6 +++
+ src/ccadical.cpp | 102 +++++++++++++++++++++++++++++++++++++++++++++++
+ src/ccadical.h   |  26 ++++++++++++
+ src/solver.cpp   |  24 +++++++++++
+ 4 files changed, 158 insertions(+)
 
 diff --git a/src/cadical.hpp b/src/cadical.hpp
 index 066c94b..fa252af 100644
@@ -28,10 +28,10 @@ index 066c94b..fa252af 100644
  
    // Enables clausal proof tracing in DRAT format and returns 'true' if
 diff --git a/src/ccadical.cpp b/src/ccadical.cpp
-index e6e7d28..0d1ebad 100644
+index e6e7d28..0c2ca8a 100644
 --- a/src/ccadical.cpp
 +++ b/src/ccadical.cpp
-@@ -177,4 +177,66 @@ int ccadical_frozen (CCaDiCaL * ptr, int lit) {
+@@ -177,4 +177,106 @@ int ccadical_frozen (CCaDiCaL * ptr, int lit) {
    return ((Wrapper*) ptr)->solver->frozen (lit);
  }
  
@@ -39,6 +39,41 @@ index e6e7d28..0d1ebad 100644
 +
 +// Extending C API (Christoph Jabs)
 +
++int ccadical_add_mem (CCaDiCaL * wrapper, int lit) {
++  try {
++    ((Wrapper*) wrapper)->solver->add (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_assume_mem (CCaDiCaL * wrapper, int lit) {
++  try {
++    ((Wrapper*) wrapper)->solver->assume (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_constrain_mem (CCaDiCaL *wrapper, int lit){
++  try {
++    ((Wrapper*) wrapper)->solver->constrain (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_solve_mem (CCaDiCaL * wrapper) {
++  try {
++    return ((Wrapper*) wrapper)->solver->solve ();
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
 +bool ccadical_configure (CCaDiCaL *ptr, const char *name) {
 +  return ((Wrapper *) ptr)->solver->configure (name);
 +}
@@ -72,8 +107,13 @@ index e6e7d28..0d1ebad 100644
 +  return ((Wrapper *) wrapper)->solver->simplify (rounds);
 +}
 +
-+void ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
-+  return ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++int ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
++  try {
++    ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
 +}
 +
 +int64_t ccadical_propagations (CCaDiCaL *wrapper) {
@@ -99,15 +139,22 @@ index e6e7d28..0d1ebad 100644
 +/*------------------------------------------------------------------------*/
  }
 diff --git a/src/ccadical.h b/src/ccadical.h
-index 332f842..4c75ce4 100644
+index 332f842..4fc2ac4 100644
 --- a/src/ccadical.h
 +++ b/src/ccadical.h
-@@ -50,6 +50,25 @@ int ccadical_simplify (CCaDiCaL *);
+@@ -50,6 +50,32 @@ int ccadical_simplify (CCaDiCaL *);
  
  /*------------------------------------------------------------------------*/
  
 +// Extending C API (Christoph Jabs)
 +
++// This value is returned from _solve_mem, _add_mem, _constrain_mem, and _assume_mem
++const int OUT_OF_MEM = 50;
++
++int ccadical_add_mem (CCaDiCaL *, int lit);
++int ccadical_assume_mem (CCaDiCaL *, int lit);
++int ccadical_constrain_mem (CCaDiCaL *, int lit);
++int ccadical_solve_mem (CCaDiCaL *);
 +bool ccadical_configure (CCaDiCaL *, const char *);
 +void ccadical_phase (CCaDiCaL *, int lit);
 +void ccadical_unphase (CCaDiCaL *, int lit);
@@ -116,7 +163,7 @@ index 332f842..4c75ce4 100644
 +bool ccadical_limit_ret (CCaDiCaL *, const char *name, int val);
 +int64_t ccadical_redundant (CCaDiCaL *);
 +int ccadical_simplify_rounds (CCaDiCaL *, int rounds);
-+void ccadical_reserve (CCaDiCaL *, int min_max_var);
++int ccadical_reserve (CCaDiCaL *, int min_max_var);
 +int64_t ccadical_propagations (CCaDiCaL *);
 +int64_t ccadical_decisions (CCaDiCaL *);
 +int64_t ccadical_conflicts (CCaDiCaL *);
@@ -164,5 +211,5 @@ index 5648101..f7e7a34 100644
  
  void Solver::freeze (int lit) {
 -- 
-2.41.0
+2.44.0
 
diff --git a/cadical/patches/v156.patch b/cadical/patches/v156.patch
index 2ff822e0..6aa6c3a4 100644
--- a/cadical/patches/v156.patch
+++ b/cadical/patches/v156.patch
@@ -1,14 +1,14 @@
-From bbbb4a0392a79340f407e816d4b368468203a052 Mon Sep 17 00:00:00 2001
+From ad523d39c9f1b187911b9c4b4e7ffd030c14821e Mon Sep 17 00:00:00 2001
 From: Christoph Jabs <christoph.jabs@helsinki.fi>
-Date: Wed, 23 Aug 2023 11:30:43 +0300
+Date: Thu, 18 Apr 2024 15:06:54 +0300
 Subject: [PATCH] extend C api
 
 ---
- src/cadical.hpp  |  6 +++++
- src/ccadical.cpp | 63 ++++++++++++++++++++++++++++++++++++++++++++++++
- src/ccadical.h   | 19 +++++++++++++++
- src/solver.cpp   | 24 ++++++++++++++++++
- 4 files changed, 112 insertions(+)
+ src/cadical.hpp  |   6 +++
+ src/ccadical.cpp | 103 +++++++++++++++++++++++++++++++++++++++++++++++
+ src/ccadical.h   |  26 ++++++++++++
+ src/solver.cpp   |  24 +++++++++++
+ 4 files changed, 159 insertions(+)
 
 diff --git a/src/cadical.hpp b/src/cadical.hpp
 index 49310c7..7e40f1d 100644
@@ -28,10 +28,10 @@ index 49310c7..7e40f1d 100644
  
    // Enables clausal proof tracing in DRAT format and returns 'true' if
 diff --git a/src/ccadical.cpp b/src/ccadical.cpp
-index ac11e44..9f7c943 100644
+index ac11e44..4caf767 100644
 --- a/src/ccadical.cpp
 +++ b/src/ccadical.cpp
-@@ -173,4 +173,67 @@ void ccadical_melt (CCaDiCaL *ptr, int lit) {
+@@ -173,4 +173,107 @@ void ccadical_melt (CCaDiCaL *ptr, int lit) {
  int ccadical_frozen (CCaDiCaL *ptr, int lit) {
    return ((Wrapper *) ptr)->solver->frozen (lit);
  }
@@ -40,6 +40,41 @@ index ac11e44..9f7c943 100644
 +
 +// Extending C API (Christoph Jabs)
 +
++int ccadical_add_mem (CCaDiCaL * wrapper, int lit) {
++  try {
++    ((Wrapper*) wrapper)->solver->add (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_assume_mem (CCaDiCaL * wrapper, int lit) {
++  try {
++    ((Wrapper*) wrapper)->solver->assume (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_constrain_mem (CCaDiCaL *wrapper, int lit){
++  try {
++    ((Wrapper*) wrapper)->solver->constrain (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_solve_mem (CCaDiCaL * wrapper) {
++  try {
++    return ((Wrapper*) wrapper)->solver->solve ();
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
 +bool ccadical_configure (CCaDiCaL *ptr, const char *name) {
 +  return ((Wrapper *) ptr)->solver->configure (name);
 +}
@@ -73,8 +108,13 @@ index ac11e44..9f7c943 100644
 +  return ((Wrapper *) wrapper)->solver->simplify (rounds);
 +}
 +
-+void ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
-+  return ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++int ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
++  try {
++    ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
 +}
 +
 +int64_t ccadical_propagations (CCaDiCaL *wrapper) {
@@ -100,15 +140,22 @@ index ac11e44..9f7c943 100644
 +/*------------------------------------------------------------------------*/
  }
 diff --git a/src/ccadical.h b/src/ccadical.h
-index 30a79b3..56fb16b 100644
+index 30a79b3..ca11867 100644
 --- a/src/ccadical.h
 +++ b/src/ccadical.h
-@@ -50,6 +50,25 @@ int ccadical_simplify (CCaDiCaL *);
+@@ -50,6 +50,32 @@ int ccadical_simplify (CCaDiCaL *);
  
  /*------------------------------------------------------------------------*/
  
 +// Extending C API (Christoph Jabs)
 +
++// This value is returned from _solve_mem, _add_mem, _constrain_mem, and _assume_mem
++const int OUT_OF_MEM = 50;
++
++int ccadical_add_mem (CCaDiCaL *, int lit);
++int ccadical_assume_mem (CCaDiCaL *, int lit);
++int ccadical_constrain_mem (CCaDiCaL *, int lit);
++int ccadical_solve_mem (CCaDiCaL *);
 +bool ccadical_configure (CCaDiCaL *, const char *);
 +void ccadical_phase (CCaDiCaL *, int lit);
 +void ccadical_unphase (CCaDiCaL *, int lit);
@@ -117,7 +164,7 @@ index 30a79b3..56fb16b 100644
 +bool ccadical_limit_ret (CCaDiCaL *, const char *name, int val);
 +int64_t ccadical_redundant (CCaDiCaL *);
 +int ccadical_simplify_rounds (CCaDiCaL *, int rounds);
-+void ccadical_reserve (CCaDiCaL *, int min_max_var);
++int ccadical_reserve (CCaDiCaL *, int min_max_var);
 +int64_t ccadical_propagations (CCaDiCaL *);
 +int64_t ccadical_decisions (CCaDiCaL *);
 +int64_t ccadical_conflicts (CCaDiCaL *);
@@ -165,5 +212,5 @@ index 63293ad..d1153d6 100644
  
  void Solver::freeze (int lit) {
 -- 
-2.41.0
+2.44.0
 
diff --git a/cadical/patches/v160.patch b/cadical/patches/v160.patch
index 1c01fc34..06d3011c 100644
--- a/cadical/patches/v160.patch
+++ b/cadical/patches/v160.patch
@@ -1,14 +1,14 @@
-From 978c6b563055207218334ea9979802d5367cc09f Mon Sep 17 00:00:00 2001
+From 6cf91b4876a3887f8d676e3092ded5debfd03682 Mon Sep 17 00:00:00 2001
 From: Christoph Jabs <christoph.jabs@helsinki.fi>
-Date: Wed, 23 Aug 2023 11:30:43 +0300
+Date: Thu, 18 Apr 2024 15:07:07 +0300
 Subject: [PATCH] extend C api
 
 ---
- src/cadical.hpp  |  6 +++++
- src/ccadical.cpp | 63 ++++++++++++++++++++++++++++++++++++++++++++++++
- src/ccadical.h   | 19 +++++++++++++++
- src/solver.cpp   | 24 ++++++++++++++++++
- 4 files changed, 112 insertions(+)
+ src/cadical.hpp  |   6 +++
+ src/ccadical.cpp | 103 +++++++++++++++++++++++++++++++++++++++++++++++
+ src/ccadical.h   |  26 ++++++++++++
+ src/solver.cpp   |  24 +++++++++++
+ 4 files changed, 159 insertions(+)
 
 diff --git a/src/cadical.hpp b/src/cadical.hpp
 index 26cb9ca..d7539fc 100644
@@ -28,10 +28,10 @@ index 26cb9ca..d7539fc 100644
  
    // Enables clausal proof tracing in DRAT format and returns 'true' if
 diff --git a/src/ccadical.cpp b/src/ccadical.cpp
-index ac11e44..9f7c943 100644
+index ac11e44..4caf767 100644
 --- a/src/ccadical.cpp
 +++ b/src/ccadical.cpp
-@@ -173,4 +173,67 @@ void ccadical_melt (CCaDiCaL *ptr, int lit) {
+@@ -173,4 +173,107 @@ void ccadical_melt (CCaDiCaL *ptr, int lit) {
  int ccadical_frozen (CCaDiCaL *ptr, int lit) {
    return ((Wrapper *) ptr)->solver->frozen (lit);
  }
@@ -40,6 +40,41 @@ index ac11e44..9f7c943 100644
 +
 +// Extending C API (Christoph Jabs)
 +
++int ccadical_add_mem (CCaDiCaL * wrapper, int lit) {
++  try {
++    ((Wrapper*) wrapper)->solver->add (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_assume_mem (CCaDiCaL * wrapper, int lit) {
++  try {
++    ((Wrapper*) wrapper)->solver->assume (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_constrain_mem (CCaDiCaL *wrapper, int lit){
++  try {
++    ((Wrapper*) wrapper)->solver->constrain (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_solve_mem (CCaDiCaL * wrapper) {
++  try {
++    return ((Wrapper*) wrapper)->solver->solve ();
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
 +bool ccadical_configure (CCaDiCaL *ptr, const char *name) {
 +  return ((Wrapper *) ptr)->solver->configure (name);
 +}
@@ -73,8 +108,13 @@ index ac11e44..9f7c943 100644
 +  return ((Wrapper *) wrapper)->solver->simplify (rounds);
 +}
 +
-+void ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
-+  return ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++int ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
++  try {
++    ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
 +}
 +
 +int64_t ccadical_propagations (CCaDiCaL *wrapper) {
@@ -100,15 +140,22 @@ index ac11e44..9f7c943 100644
 +/*------------------------------------------------------------------------*/
  }
 diff --git a/src/ccadical.h b/src/ccadical.h
-index 30a79b3..56fb16b 100644
+index 30a79b3..ca11867 100644
 --- a/src/ccadical.h
 +++ b/src/ccadical.h
-@@ -50,6 +50,25 @@ int ccadical_simplify (CCaDiCaL *);
+@@ -50,6 +50,32 @@ int ccadical_simplify (CCaDiCaL *);
  
  /*------------------------------------------------------------------------*/
  
 +// Extending C API (Christoph Jabs)
 +
++// This value is returned from _solve_mem, _add_mem, _constrain_mem, and _assume_mem
++const int OUT_OF_MEM = 50;
++
++int ccadical_add_mem (CCaDiCaL *, int lit);
++int ccadical_assume_mem (CCaDiCaL *, int lit);
++int ccadical_constrain_mem (CCaDiCaL *, int lit);
++int ccadical_solve_mem (CCaDiCaL *);
 +bool ccadical_configure (CCaDiCaL *, const char *);
 +void ccadical_phase (CCaDiCaL *, int lit);
 +void ccadical_unphase (CCaDiCaL *, int lit);
@@ -117,7 +164,7 @@ index 30a79b3..56fb16b 100644
 +bool ccadical_limit_ret (CCaDiCaL *, const char *name, int val);
 +int64_t ccadical_redundant (CCaDiCaL *);
 +int ccadical_simplify_rounds (CCaDiCaL *, int rounds);
-+void ccadical_reserve (CCaDiCaL *, int min_max_var);
++int ccadical_reserve (CCaDiCaL *, int min_max_var);
 +int64_t ccadical_propagations (CCaDiCaL *);
 +int64_t ccadical_decisions (CCaDiCaL *);
 +int64_t ccadical_conflicts (CCaDiCaL *);
@@ -165,5 +212,5 @@ index 9ac3887..fd964fd 100644
  
  void Solver::freeze (int lit) {
 -- 
-2.41.0
+2.44.0
 
diff --git a/cadical/patches/v170.patch b/cadical/patches/v170.patch
index 4a04bba8..81a9cb23 100644
--- a/cadical/patches/v170.patch
+++ b/cadical/patches/v170.patch
@@ -1,14 +1,14 @@
-From 9f5fe5b55adccf8ff01a6e2934983f61d78a91c7 Mon Sep 17 00:00:00 2001
+From 3587ae5e0ef8385c9736caa1c00b15b999ff67d3 Mon Sep 17 00:00:00 2001
 From: Christoph Jabs <christoph.jabs@helsinki.fi>
-Date: Wed, 23 Aug 2023 11:30:43 +0300
+Date: Thu, 18 Apr 2024 15:07:29 +0300
 Subject: [PATCH] extend C api
 
 ---
- src/cadical.hpp  |  6 +++++
- src/ccadical.cpp | 63 ++++++++++++++++++++++++++++++++++++++++++++++++
- src/ccadical.h   | 19 +++++++++++++++
- src/solver.cpp   | 24 ++++++++++++++++++
- 4 files changed, 112 insertions(+)
+ src/cadical.hpp  |   6 +++
+ src/ccadical.cpp | 103 +++++++++++++++++++++++++++++++++++++++++++++++
+ src/ccadical.h   |  26 ++++++++++++
+ src/solver.cpp   |  24 +++++++++++
+ 4 files changed, 159 insertions(+)
 
 diff --git a/src/cadical.hpp b/src/cadical.hpp
 index 26cb9ca..d7539fc 100644
@@ -28,10 +28,10 @@ index 26cb9ca..d7539fc 100644
  
    // Enables clausal proof tracing in DRAT format and returns 'true' if
 diff --git a/src/ccadical.cpp b/src/ccadical.cpp
-index ac11e44..9f7c943 100644
+index ac11e44..4caf767 100644
 --- a/src/ccadical.cpp
 +++ b/src/ccadical.cpp
-@@ -173,4 +173,67 @@ void ccadical_melt (CCaDiCaL *ptr, int lit) {
+@@ -173,4 +173,107 @@ void ccadical_melt (CCaDiCaL *ptr, int lit) {
  int ccadical_frozen (CCaDiCaL *ptr, int lit) {
    return ((Wrapper *) ptr)->solver->frozen (lit);
  }
@@ -40,6 +40,41 @@ index ac11e44..9f7c943 100644
 +
 +// Extending C API (Christoph Jabs)
 +
++int ccadical_add_mem (CCaDiCaL * wrapper, int lit) {
++  try {
++    ((Wrapper*) wrapper)->solver->add (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_assume_mem (CCaDiCaL * wrapper, int lit) {
++  try {
++    ((Wrapper*) wrapper)->solver->assume (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_constrain_mem (CCaDiCaL *wrapper, int lit){
++  try {
++    ((Wrapper*) wrapper)->solver->constrain (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_solve_mem (CCaDiCaL * wrapper) {
++  try {
++    return ((Wrapper*) wrapper)->solver->solve ();
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
 +bool ccadical_configure (CCaDiCaL *ptr, const char *name) {
 +  return ((Wrapper *) ptr)->solver->configure (name);
 +}
@@ -73,8 +108,13 @@ index ac11e44..9f7c943 100644
 +  return ((Wrapper *) wrapper)->solver->simplify (rounds);
 +}
 +
-+void ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
-+  return ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++int ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
++  try {
++    ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
 +}
 +
 +int64_t ccadical_propagations (CCaDiCaL *wrapper) {
@@ -100,15 +140,22 @@ index ac11e44..9f7c943 100644
 +/*------------------------------------------------------------------------*/
  }
 diff --git a/src/ccadical.h b/src/ccadical.h
-index 30a79b3..56fb16b 100644
+index 30a79b3..ca11867 100644
 --- a/src/ccadical.h
 +++ b/src/ccadical.h
-@@ -50,6 +50,25 @@ int ccadical_simplify (CCaDiCaL *);
+@@ -50,6 +50,32 @@ int ccadical_simplify (CCaDiCaL *);
  
  /*------------------------------------------------------------------------*/
  
 +// Extending C API (Christoph Jabs)
 +
++// This value is returned from _solve_mem, _add_mem, _constrain_mem, and _assume_mem
++const int OUT_OF_MEM = 50;
++
++int ccadical_add_mem (CCaDiCaL *, int lit);
++int ccadical_assume_mem (CCaDiCaL *, int lit);
++int ccadical_constrain_mem (CCaDiCaL *, int lit);
++int ccadical_solve_mem (CCaDiCaL *);
 +bool ccadical_configure (CCaDiCaL *, const char *);
 +void ccadical_phase (CCaDiCaL *, int lit);
 +void ccadical_unphase (CCaDiCaL *, int lit);
@@ -117,7 +164,7 @@ index 30a79b3..56fb16b 100644
 +bool ccadical_limit_ret (CCaDiCaL *, const char *name, int val);
 +int64_t ccadical_redundant (CCaDiCaL *);
 +int ccadical_simplify_rounds (CCaDiCaL *, int rounds);
-+void ccadical_reserve (CCaDiCaL *, int min_max_var);
++int ccadical_reserve (CCaDiCaL *, int min_max_var);
 +int64_t ccadical_propagations (CCaDiCaL *);
 +int64_t ccadical_decisions (CCaDiCaL *);
 +int64_t ccadical_conflicts (CCaDiCaL *);
@@ -165,5 +212,5 @@ index 3887a97..6b1727b 100644
  
  void Solver::freeze (int lit) {
 -- 
-2.41.0
+2.44.0
 
diff --git a/cadical/patches/v171.patch b/cadical/patches/v171.patch
index 645b4c13..bc6231d2 100644
--- a/cadical/patches/v171.patch
+++ b/cadical/patches/v171.patch
@@ -1,14 +1,14 @@
-From 1f7e50a76d83dd4c8d6cf9a7c7e129af2d8ad34c Mon Sep 17 00:00:00 2001
+From f3f9648731952547da82db36544d59916032da78 Mon Sep 17 00:00:00 2001
 From: Christoph Jabs <christoph.jabs@helsinki.fi>
-Date: Mon, 4 Sep 2023 10:53:33 +0300
+Date: Thu, 18 Apr 2024 15:07:50 +0300
 Subject: [PATCH] extend C api
 
 ---
- src/cadical.hpp  |  6 +++++
- src/ccadical.cpp | 63 ++++++++++++++++++++++++++++++++++++++++++++++++
- src/ccadical.h   | 19 +++++++++++++++
- src/solver.cpp   | 24 ++++++++++++++++++
- 4 files changed, 112 insertions(+)
+ src/cadical.hpp  |   6 +++
+ src/ccadical.cpp | 103 +++++++++++++++++++++++++++++++++++++++++++++++
+ src/ccadical.h   |  26 ++++++++++++
+ src/solver.cpp   |  24 +++++++++++
+ 4 files changed, 159 insertions(+)
 
 diff --git a/src/cadical.hpp b/src/cadical.hpp
 index 0991695..d6b9357 100644
@@ -28,10 +28,10 @@ index 0991695..d6b9357 100644
  
    // Enables clausal proof tracing in DRAT format and returns 'true' if
 diff --git a/src/ccadical.cpp b/src/ccadical.cpp
-index ac11e44..9f7c943 100644
+index ac11e44..4caf767 100644
 --- a/src/ccadical.cpp
 +++ b/src/ccadical.cpp
-@@ -173,4 +173,67 @@ void ccadical_melt (CCaDiCaL *ptr, int lit) {
+@@ -173,4 +173,107 @@ void ccadical_melt (CCaDiCaL *ptr, int lit) {
  int ccadical_frozen (CCaDiCaL *ptr, int lit) {
    return ((Wrapper *) ptr)->solver->frozen (lit);
  }
@@ -40,6 +40,41 @@ index ac11e44..9f7c943 100644
 +
 +// Extending C API (Christoph Jabs)
 +
++int ccadical_add_mem (CCaDiCaL * wrapper, int lit) {
++  try {
++    ((Wrapper*) wrapper)->solver->add (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_assume_mem (CCaDiCaL * wrapper, int lit) {
++  try {
++    ((Wrapper*) wrapper)->solver->assume (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_constrain_mem (CCaDiCaL *wrapper, int lit){
++  try {
++    ((Wrapper*) wrapper)->solver->constrain (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_solve_mem (CCaDiCaL * wrapper) {
++  try {
++    return ((Wrapper*) wrapper)->solver->solve ();
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
 +bool ccadical_configure (CCaDiCaL *ptr, const char *name) {
 +  return ((Wrapper *) ptr)->solver->configure (name);
 +}
@@ -73,8 +108,13 @@ index ac11e44..9f7c943 100644
 +  return ((Wrapper *) wrapper)->solver->simplify (rounds);
 +}
 +
-+void ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
-+  return ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++int ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
++  try {
++    ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
 +}
 +
 +int64_t ccadical_propagations (CCaDiCaL *wrapper) {
@@ -100,15 +140,22 @@ index ac11e44..9f7c943 100644
 +/*------------------------------------------------------------------------*/
  }
 diff --git a/src/ccadical.h b/src/ccadical.h
-index 30a79b3..56fb16b 100644
+index 30a79b3..ca11867 100644
 --- a/src/ccadical.h
 +++ b/src/ccadical.h
-@@ -50,6 +50,25 @@ int ccadical_simplify (CCaDiCaL *);
+@@ -50,6 +50,32 @@ int ccadical_simplify (CCaDiCaL *);
  
  /*------------------------------------------------------------------------*/
  
 +// Extending C API (Christoph Jabs)
 +
++// This value is returned from _solve_mem, _add_mem, _constrain_mem, and _assume_mem
++const int OUT_OF_MEM = 50;
++
++int ccadical_add_mem (CCaDiCaL *, int lit);
++int ccadical_assume_mem (CCaDiCaL *, int lit);
++int ccadical_constrain_mem (CCaDiCaL *, int lit);
++int ccadical_solve_mem (CCaDiCaL *);
 +bool ccadical_configure (CCaDiCaL *, const char *);
 +void ccadical_phase (CCaDiCaL *, int lit);
 +void ccadical_unphase (CCaDiCaL *, int lit);
@@ -117,7 +164,7 @@ index 30a79b3..56fb16b 100644
 +bool ccadical_limit_ret (CCaDiCaL *, const char *name, int val);
 +int64_t ccadical_redundant (CCaDiCaL *);
 +int ccadical_simplify_rounds (CCaDiCaL *, int rounds);
-+void ccadical_reserve (CCaDiCaL *, int min_max_var);
++int ccadical_reserve (CCaDiCaL *, int min_max_var);
 +int64_t ccadical_propagations (CCaDiCaL *);
 +int64_t ccadical_decisions (CCaDiCaL *);
 +int64_t ccadical_conflicts (CCaDiCaL *);
@@ -165,5 +212,5 @@ index 5a5733c..4cbf0bb 100644
  
  void Solver::freeze (int lit) {
 -- 
-2.41.0
+2.44.0
 
diff --git a/cadical/patches/v180.patch b/cadical/patches/v180.patch
index 6f846f0a..74155960 100644
--- a/cadical/patches/v180.patch
+++ b/cadical/patches/v180.patch
@@ -1,14 +1,14 @@
-From e83aaf6d9a15bb93ac2c802c44f5b51c235f3912 Mon Sep 17 00:00:00 2001
+From 30acbccfcc4dd30dde3c39a022a019045c8dca2b Mon Sep 17 00:00:00 2001
 From: Christoph Jabs <christoph.jabs@helsinki.fi>
-Date: Tue, 3 Oct 2023 13:39:32 +0300
+Date: Thu, 18 Apr 2024 15:08:09 +0300
 Subject: [PATCH] extend C api
 
 ---
- src/cadical.hpp  |  6 +++++
- src/ccadical.cpp | 63 ++++++++++++++++++++++++++++++++++++++++++++++++
- src/ccadical.h   | 19 +++++++++++++++
- src/solver.cpp   | 24 ++++++++++++++++++
- 4 files changed, 112 insertions(+)
+ src/cadical.hpp  |   6 +++
+ src/ccadical.cpp | 103 +++++++++++++++++++++++++++++++++++++++++++++++
+ src/ccadical.h   |  26 ++++++++++++
+ src/solver.cpp   |  24 +++++++++++
+ 4 files changed, 159 insertions(+)
 
 diff --git a/src/cadical.hpp b/src/cadical.hpp
 index 0ce3e82..5857d3a 100644
@@ -28,10 +28,10 @@ index 0ce3e82..5857d3a 100644
  
    // Enables clausal proof tracing in DRAT format and returns 'true' if
 diff --git a/src/ccadical.cpp b/src/ccadical.cpp
-index ac11e44..9f7c943 100644
+index ac11e44..4caf767 100644
 --- a/src/ccadical.cpp
 +++ b/src/ccadical.cpp
-@@ -173,4 +173,67 @@ void ccadical_melt (CCaDiCaL *ptr, int lit) {
+@@ -173,4 +173,107 @@ void ccadical_melt (CCaDiCaL *ptr, int lit) {
  int ccadical_frozen (CCaDiCaL *ptr, int lit) {
    return ((Wrapper *) ptr)->solver->frozen (lit);
  }
@@ -40,6 +40,41 @@ index ac11e44..9f7c943 100644
 +
 +// Extending C API (Christoph Jabs)
 +
++int ccadical_add_mem (CCaDiCaL * wrapper, int lit) {
++  try {
++    ((Wrapper*) wrapper)->solver->add (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_assume_mem (CCaDiCaL * wrapper, int lit) {
++  try {
++    ((Wrapper*) wrapper)->solver->assume (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_constrain_mem (CCaDiCaL *wrapper, int lit){
++  try {
++    ((Wrapper*) wrapper)->solver->constrain (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_solve_mem (CCaDiCaL * wrapper) {
++  try {
++    return ((Wrapper*) wrapper)->solver->solve ();
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
 +bool ccadical_configure (CCaDiCaL *ptr, const char *name) {
 +  return ((Wrapper *) ptr)->solver->configure (name);
 +}
@@ -73,8 +108,13 @@ index ac11e44..9f7c943 100644
 +  return ((Wrapper *) wrapper)->solver->simplify (rounds);
 +}
 +
-+void ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
-+  return ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++int ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
++  try {
++    ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
 +}
 +
 +int64_t ccadical_propagations (CCaDiCaL *wrapper) {
@@ -100,15 +140,22 @@ index ac11e44..9f7c943 100644
 +/*------------------------------------------------------------------------*/
  }
 diff --git a/src/ccadical.h b/src/ccadical.h
-index 30a79b3..56fb16b 100644
+index 30a79b3..ca11867 100644
 --- a/src/ccadical.h
 +++ b/src/ccadical.h
-@@ -50,6 +50,25 @@ int ccadical_simplify (CCaDiCaL *);
+@@ -50,6 +50,32 @@ int ccadical_simplify (CCaDiCaL *);
  
  /*------------------------------------------------------------------------*/
  
 +// Extending C API (Christoph Jabs)
 +
++// This value is returned from _solve_mem, _add_mem, _constrain_mem, and _assume_mem
++const int OUT_OF_MEM = 50;
++
++int ccadical_add_mem (CCaDiCaL *, int lit);
++int ccadical_assume_mem (CCaDiCaL *, int lit);
++int ccadical_constrain_mem (CCaDiCaL *, int lit);
++int ccadical_solve_mem (CCaDiCaL *);
 +bool ccadical_configure (CCaDiCaL *, const char *);
 +void ccadical_phase (CCaDiCaL *, int lit);
 +void ccadical_unphase (CCaDiCaL *, int lit);
@@ -117,7 +164,7 @@ index 30a79b3..56fb16b 100644
 +bool ccadical_limit_ret (CCaDiCaL *, const char *name, int val);
 +int64_t ccadical_redundant (CCaDiCaL *);
 +int ccadical_simplify_rounds (CCaDiCaL *, int rounds);
-+void ccadical_reserve (CCaDiCaL *, int min_max_var);
++int ccadical_reserve (CCaDiCaL *, int min_max_var);
 +int64_t ccadical_propagations (CCaDiCaL *);
 +int64_t ccadical_decisions (CCaDiCaL *);
 +int64_t ccadical_conflicts (CCaDiCaL *);
@@ -165,5 +212,5 @@ index 520664d..72e56dc 100644
  
  void Solver::freeze (int lit) {
 -- 
-2.41.0
+2.44.0
 
diff --git a/cadical/patches/v190.patch b/cadical/patches/v190.patch
index ebfd9ffd..61a9b3a5 100644
--- a/cadical/patches/v190.patch
+++ b/cadical/patches/v190.patch
@@ -1,14 +1,14 @@
-From d19b6b97766982fe80b4ff8d030d34ffedede473 Mon Sep 17 00:00:00 2001
+From 660b1b5950f0d2872a47b89c2bd4aa73acdd8a5e Mon Sep 17 00:00:00 2001
 From: Christoph Jabs <christoph.jabs@helsinki.fi>
-Date: Mon, 18 Dec 2023 10:35:19 +0200
+Date: Thu, 18 Apr 2024 15:08:22 +0300
 Subject: [PATCH] extend C api
 
 ---
- src/cadical.hpp  |  6 +++++
- src/ccadical.cpp | 63 ++++++++++++++++++++++++++++++++++++++++++++++++
- src/ccadical.h   | 19 +++++++++++++++
- src/solver.cpp   | 24 ++++++++++++++++++
- 4 files changed, 112 insertions(+)
+ src/cadical.hpp  |   6 +++
+ src/ccadical.cpp | 103 +++++++++++++++++++++++++++++++++++++++++++++++
+ src/ccadical.h   |  26 ++++++++++++
+ src/solver.cpp   |  24 +++++++++++
+ 4 files changed, 159 insertions(+)
 
 diff --git a/src/cadical.hpp b/src/cadical.hpp
 index 3270592..dc125d7 100644
@@ -28,10 +28,10 @@ index 3270592..dc125d7 100644
  
    // Enables clausal proof tracing in DRAT format and returns 'true' if
 diff --git a/src/ccadical.cpp b/src/ccadical.cpp
-index ac11e44..9f7c943 100644
+index ac11e44..4caf767 100644
 --- a/src/ccadical.cpp
 +++ b/src/ccadical.cpp
-@@ -173,4 +173,67 @@ void ccadical_melt (CCaDiCaL *ptr, int lit) {
+@@ -173,4 +173,107 @@ void ccadical_melt (CCaDiCaL *ptr, int lit) {
  int ccadical_frozen (CCaDiCaL *ptr, int lit) {
    return ((Wrapper *) ptr)->solver->frozen (lit);
  }
@@ -40,6 +40,41 @@ index ac11e44..9f7c943 100644
 +
 +// Extending C API (Christoph Jabs)
 +
++int ccadical_add_mem (CCaDiCaL * wrapper, int lit) {
++  try {
++    ((Wrapper*) wrapper)->solver->add (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_assume_mem (CCaDiCaL * wrapper, int lit) {
++  try {
++    ((Wrapper*) wrapper)->solver->assume (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_constrain_mem (CCaDiCaL *wrapper, int lit){
++  try {
++    ((Wrapper*) wrapper)->solver->constrain (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_solve_mem (CCaDiCaL * wrapper) {
++  try {
++    return ((Wrapper*) wrapper)->solver->solve ();
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
 +bool ccadical_configure (CCaDiCaL *ptr, const char *name) {
 +  return ((Wrapper *) ptr)->solver->configure (name);
 +}
@@ -73,8 +108,13 @@ index ac11e44..9f7c943 100644
 +  return ((Wrapper *) wrapper)->solver->simplify (rounds);
 +}
 +
-+void ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
-+  return ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++int ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
++  try {
++    ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
 +}
 +
 +int64_t ccadical_propagations (CCaDiCaL *wrapper) {
@@ -100,15 +140,22 @@ index ac11e44..9f7c943 100644
 +/*------------------------------------------------------------------------*/
  }
 diff --git a/src/ccadical.h b/src/ccadical.h
-index 30a79b3..56fb16b 100644
+index 30a79b3..ca11867 100644
 --- a/src/ccadical.h
 +++ b/src/ccadical.h
-@@ -50,6 +50,25 @@ int ccadical_simplify (CCaDiCaL *);
+@@ -50,6 +50,32 @@ int ccadical_simplify (CCaDiCaL *);
  
  /*------------------------------------------------------------------------*/
  
 +// Extending C API (Christoph Jabs)
 +
++// This value is returned from _solve_mem, _add_mem, _constrain_mem, and _assume_mem
++const int OUT_OF_MEM = 50;
++
++int ccadical_add_mem (CCaDiCaL *, int lit);
++int ccadical_assume_mem (CCaDiCaL *, int lit);
++int ccadical_constrain_mem (CCaDiCaL *, int lit);
++int ccadical_solve_mem (CCaDiCaL *);
 +bool ccadical_configure (CCaDiCaL *, const char *);
 +void ccadical_phase (CCaDiCaL *, int lit);
 +void ccadical_unphase (CCaDiCaL *, int lit);
@@ -117,7 +164,7 @@ index 30a79b3..56fb16b 100644
 +bool ccadical_limit_ret (CCaDiCaL *, const char *name, int val);
 +int64_t ccadical_redundant (CCaDiCaL *);
 +int ccadical_simplify_rounds (CCaDiCaL *, int rounds);
-+void ccadical_reserve (CCaDiCaL *, int min_max_var);
++int ccadical_reserve (CCaDiCaL *, int min_max_var);
 +int64_t ccadical_propagations (CCaDiCaL *);
 +int64_t ccadical_decisions (CCaDiCaL *);
 +int64_t ccadical_conflicts (CCaDiCaL *);
@@ -165,5 +212,5 @@ index 590d3f1..1ec241e 100644
  
  void Solver::freeze (int lit) {
 -- 
-2.43.0
+2.44.0
 
diff --git a/cadical/patches/v192.patch b/cadical/patches/v192.patch
index 279df042..4f454e4e 100644
--- a/cadical/patches/v192.patch
+++ b/cadical/patches/v192.patch
@@ -1,14 +1,14 @@
-From d68b6ded46632f026f812efc00a23c345083788f Mon Sep 17 00:00:00 2001
+From 6b7a1295f3703bf640009206310fcb9b69f14a68 Mon Sep 17 00:00:00 2001
 From: Christoph Jabs <christoph.jabs@helsinki.fi>
-Date: Mon, 18 Dec 2023 10:44:47 +0200
+Date: Thu, 18 Apr 2024 15:09:21 +0300
 Subject: [PATCH] extend C api
 
 ---
- src/cadical.hpp  |  6 +++++
- src/ccadical.cpp | 63 ++++++++++++++++++++++++++++++++++++++++++++++++
- src/ccadical.h   | 19 +++++++++++++++
- src/solver.cpp   | 24 ++++++++++++++++++
- 4 files changed, 112 insertions(+)
+ src/cadical.hpp  |   6 +++
+ src/ccadical.cpp | 103 +++++++++++++++++++++++++++++++++++++++++++++++
+ src/ccadical.h   |  26 ++++++++++++
+ src/solver.cpp   |  24 +++++++++++
+ 4 files changed, 159 insertions(+)
 
 diff --git a/src/cadical.hpp b/src/cadical.hpp
 index a803292..8520e2b 100644
@@ -28,10 +28,10 @@ index a803292..8520e2b 100644
  
    // Enables clausal proof tracing in DRAT format and returns 'true' if
 diff --git a/src/ccadical.cpp b/src/ccadical.cpp
-index 88ab164..54798d7 100644
+index 88ab164..846467e 100644
 --- a/src/ccadical.cpp
 +++ b/src/ccadical.cpp
-@@ -185,4 +185,67 @@ void ccadical_close_proof (CCaDiCaL *ptr) {
+@@ -185,4 +185,107 @@ void ccadical_close_proof (CCaDiCaL *ptr) {
  void ccadical_conclude (CCaDiCaL *ptr) {
    ((Wrapper *) ptr)->solver->conclude ();
  }
@@ -40,6 +40,41 @@ index 88ab164..54798d7 100644
 +
 +// Extending C API (Christoph Jabs)
 +
++int ccadical_add_mem (CCaDiCaL * wrapper, int lit) {
++  try {
++    ((Wrapper*) wrapper)->solver->add (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_assume_mem (CCaDiCaL * wrapper, int lit) {
++  try {
++    ((Wrapper*) wrapper)->solver->assume (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_constrain_mem (CCaDiCaL *wrapper, int lit){
++  try {
++    ((Wrapper*) wrapper)->solver->constrain (lit);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
++int ccadical_solve_mem (CCaDiCaL * wrapper) {
++  try {
++    return ((Wrapper*) wrapper)->solver->solve ();
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
++}
++
 +bool ccadical_configure (CCaDiCaL *ptr, const char *name) {
 +  return ((Wrapper *) ptr)->solver->configure (name);
 +}
@@ -73,8 +108,13 @@ index 88ab164..54798d7 100644
 +  return ((Wrapper *) wrapper)->solver->simplify (rounds);
 +}
 +
-+void ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
-+  return ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++int ccadical_reserve (CCaDiCaL *wrapper, int min_max_var) {
++  try {
++    ((Wrapper *) wrapper)->solver->reserve (min_max_var);
++    return 0;
++  } catch (std::bad_alloc &) {
++    return OUT_OF_MEM;
++  }
 +}
 +
 +int64_t ccadical_propagations (CCaDiCaL *wrapper) {
@@ -100,15 +140,22 @@ index 88ab164..54798d7 100644
 +/*------------------------------------------------------------------------*/
  }
 diff --git a/src/ccadical.h b/src/ccadical.h
-index 6d1b3ff..7f6892b 100644
+index 6d1b3ff..f9a58a2 100644
 --- a/src/ccadical.h
 +++ b/src/ccadical.h
-@@ -54,6 +54,25 @@ int ccadical_simplify (CCaDiCaL *);
+@@ -54,6 +54,32 @@ int ccadical_simplify (CCaDiCaL *);
  
  /*------------------------------------------------------------------------*/
  
 +// Extending C API (Christoph Jabs)
 +
++// This value is returned from _solve_mem, _add_mem, _constrain_mem, and _assume_mem
++const int OUT_OF_MEM = 50;
++
++int ccadical_add_mem (CCaDiCaL *, int lit);
++int ccadical_assume_mem (CCaDiCaL *, int lit);
++int ccadical_constrain_mem (CCaDiCaL *, int lit);
++int ccadical_solve_mem (CCaDiCaL *);
 +bool ccadical_configure (CCaDiCaL *, const char *);
 +void ccadical_phase (CCaDiCaL *, int lit);
 +void ccadical_unphase (CCaDiCaL *, int lit);
@@ -117,7 +164,7 @@ index 6d1b3ff..7f6892b 100644
 +bool ccadical_limit_ret (CCaDiCaL *, const char *name, int val);
 +int64_t ccadical_redundant (CCaDiCaL *);
 +int ccadical_simplify_rounds (CCaDiCaL *, int rounds);
-+void ccadical_reserve (CCaDiCaL *, int min_max_var);
++int ccadical_reserve (CCaDiCaL *, int min_max_var);
 +int64_t ccadical_propagations (CCaDiCaL *);
 +int64_t ccadical_decisions (CCaDiCaL *);
 +int64_t ccadical_conflicts (CCaDiCaL *);
@@ -165,5 +212,5 @@ index a2505ee..b5a375c 100644
  
  void Solver::freeze (int lit) {
 -- 
-2.43.0
+2.44.0
 
diff --git a/cadical/src/lib.rs b/cadical/src/lib.rs
index 0dad88a3..69a736e5 100644
--- a/cadical/src/lib.rs
+++ b/cadical/src/lib.rs
@@ -35,6 +35,29 @@ use rustsat::solvers::{
 use rustsat::types::{Clause, Lit, TernaryVal, Var};
 use thiserror::Error;
 
+const OUT_OF_MEM: c_int = 50;
+
+macro_rules! handle_oom {
+    ($val:expr) => {{
+        let val = $val;
+        if val == crate::OUT_OF_MEM {
+            return anyhow::Context::context(
+                Err(rustsat::OutOfMemory::ExternalApi),
+                "cadical out of memory",
+            );
+        }
+        val
+    }};
+    ($val:expr, noanyhow) => {{
+        let val = $val;
+        if val == crate::OUT_OF_MEM {
+            return Err(rustsat::OutOfMemory::ExternalApi);
+        }
+        val
+    }};
+}
+pub(crate) use handle_oom;
+
 /// Fatal error returned if the CaDiCaL API returns an invalid value
 #[derive(Error, Clone, Copy, PartialEq, Eq, Debug)]
 #[error("cadical c-api returned an invalid value: {api_call} -> {value}")]
@@ -83,6 +106,10 @@ unsafe impl Send for CaDiCaL<'_, '_> {}
 
 impl Default for CaDiCaL<'_, '_> {
     fn default() -> Self {
+        let handle = unsafe { ffi::ccadical_init() };
+        if handle.is_null() {
+            panic!("not enough memory to initialize CaDiCaL solver")
+        }
         let solver = Self {
             handle: unsafe { ffi::ccadical_init() },
             state: Default::default(),
@@ -120,7 +147,7 @@ impl CaDiCaL<'_, '_> {
     /// _Note_: If this is used, in addition to [`SolveIncremental::core`],
     /// [`CaDiCaL::tmp_clause_in_core`] needs to be checked to determine if the
     /// temporary clause is part of the core.
-    pub fn add_tmp_clause(&mut self, clause: Clause) {
+    pub fn add_tmp_clause(&mut self, clause: Clause) -> Result<(), rustsat::OutOfMemory> {
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         self.stats.avg_clause_len =
@@ -129,9 +156,16 @@ impl CaDiCaL<'_, '_> {
         self.state = InternalSolverState::Input;
         // Call CaDiCaL backend
         for lit in &clause {
-            unsafe { ffi::ccadical_constrain(self.handle, lit.to_ipasir()) }
+            handle_oom!(
+                unsafe { ffi::ccadical_constrain_mem(self.handle, lit.to_ipasir()) },
+                noanyhow
+            );
         }
-        unsafe { ffi::ccadical_constrain(self.handle, 0) }
+        handle_oom!(
+            unsafe { ffi::ccadical_constrain_mem(self.handle, 0) },
+            noanyhow
+        );
+        Ok(())
     }
 
     /// Checks whether the temporary clause is part of the core if in
@@ -347,7 +381,7 @@ impl CaDiCaL<'_, '_> {
         let rounds: c_int = rounds.try_into()?;
         // Simplify with CaDiCaL backend under assumptions
         for a in &assumps {
-            unsafe { ffi::ccadical_assume(self.handle, a.to_ipasir()) }
+            handle_oom!(unsafe { ffi::ccadical_assume_mem(self.handle, a.to_ipasir()) });
         }
         match unsafe { ffi::ccadical_simplify_rounds(self.handle, rounds) } {
             0 => {
@@ -398,7 +432,7 @@ impl Solve for CaDiCaL<'_, '_> {
 
     fn reserve(&mut self, max_var: Var) -> anyhow::Result<()> {
         self.state = InternalSolverState::Input;
-        unsafe { ffi::ccadical_reserve(self.handle, max_var.to_ipasir()) };
+        handle_oom!(unsafe { ffi::ccadical_reserve(self.handle, max_var.to_ipasir()) });
         Ok(())
     }
 
@@ -414,7 +448,7 @@ impl Solve for CaDiCaL<'_, '_> {
         }
         let start = ProcessTime::now();
         // Solve with CaDiCaL backend
-        let res = unsafe { ffi::ccadical_solve(self.handle) };
+        let res = handle_oom!(unsafe { ffi::ccadical_solve_mem(self.handle) });
         self.stats.cpu_solve_time += start.elapsed();
         match res {
             0 => {
@@ -471,10 +505,10 @@ impl Solve for CaDiCaL<'_, '_> {
                 / self.stats.n_clauses as f32;
         self.state = InternalSolverState::Input;
         // Call CaDiCaL backend
-        clause
-            .iter()
-            .for_each(|l| unsafe { ffi::ccadical_add(self.handle, l.to_ipasir()) });
-        unsafe { ffi::ccadical_add(self.handle, 0) };
+        for &l in clause {
+            handle_oom!(unsafe { ffi::ccadical_add_mem(self.handle, l.to_ipasir()) });
+        }
+        handle_oom!(unsafe { ffi::ccadical_add_mem(self.handle, 0) });
         Ok(())
     }
 }
@@ -484,9 +518,9 @@ impl SolveIncremental for CaDiCaL<'_, '_> {
         let start = ProcessTime::now();
         // Solve with CaDiCaL backend
         for a in assumps {
-            unsafe { ffi::ccadical_assume(self.handle, a.to_ipasir()) }
+            handle_oom!(unsafe { ffi::ccadical_assume_mem(self.handle, a.to_ipasir()) });
         }
-        let res = unsafe { ffi::ccadical_solve(self.handle) };
+        let res = handle_oom!(unsafe { ffi::ccadical_solve_mem(self.handle) });
         self.stats.cpu_solve_time += start.elapsed();
         match res {
             0 => {
@@ -674,18 +708,11 @@ impl FreezeVar for CaDiCaL<'_, '_> {
 }
 
 // >= v1.5.4
-#[cfg(any(
-    feature = "v1-5-4",
-    feature = "v1-5-5",
-    feature = "v1-5-6",
-    feature = "v1-6-0",
-    feature = "v1-7-0",
-    all(
-        not(feature = "v1-5-3"),
-        not(feature = "v1-5-2"),
-        not(feature = "v1-5-1"),
-        not(feature = "v1-5-0")
-    )
+#[cfg(all(
+    not(feature = "v1-5-3"),
+    not(feature = "v1-5-2"),
+    not(feature = "v1-5-1"),
+    not(feature = "v1-5-0")
 ))]
 impl rustsat::solvers::FlipLit for CaDiCaL<'_, '_> {
     fn flip_lit(&mut self, lit: Lit) -> anyhow::Result<bool> {
@@ -915,9 +942,9 @@ mod ffi {
         pub fn ccadical_signature() -> *const c_char;
         pub fn ccadical_init() -> *mut CaDiCaLHandle;
         pub fn ccadical_release(solver: *mut CaDiCaLHandle);
-        pub fn ccadical_add(solver: *mut CaDiCaLHandle, lit_or_zero: c_int);
-        pub fn ccadical_assume(solver: *mut CaDiCaLHandle, lit: c_int);
-        pub fn ccadical_solve(solver: *mut CaDiCaLHandle) -> c_int;
+        pub fn ccadical_add_mem(solver: *mut CaDiCaLHandle, lit_or_zero: c_int) -> c_int;
+        pub fn ccadical_assume_mem(solver: *mut CaDiCaLHandle, lit: c_int) -> c_int;
+        pub fn ccadical_solve_mem(solver: *mut CaDiCaLHandle) -> c_int;
         pub fn ccadical_val(solver: *mut CaDiCaLHandle, lit: c_int) -> c_int;
         pub fn ccadical_failed(solver: *mut CaDiCaLHandle, lit: c_int) -> c_int;
         pub fn ccadical_set_terminate(
@@ -931,7 +958,7 @@ mod ffi {
             max_length: c_int,
             learn: Option<extern "C" fn(state: *const c_void, clause: *const c_int)>,
         );
-        pub fn ccadical_constrain(solver: *mut CaDiCaLHandle, lit: c_int);
+        pub fn ccadical_constrain_mem(solver: *mut CaDiCaLHandle, lit: c_int) -> c_int;
         pub fn ccadical_constraint_failed(solver: *mut CaDiCaLHandle) -> c_int;
         pub fn ccadical_set_option_ret(
             solver: *mut CaDiCaLHandle,
@@ -958,25 +985,18 @@ mod ffi {
         pub fn ccadical_phase(solver: *mut CaDiCaLHandle, lit: c_int);
         pub fn ccadical_unphase(solver: *mut CaDiCaLHandle, lit: c_int);
         pub fn ccadical_vars(solver: *mut CaDiCaLHandle) -> c_int;
-        pub fn ccadical_reserve(solver: *mut CaDiCaLHandle, min_max_var: c_int);
+        pub fn ccadical_reserve(solver: *mut CaDiCaLHandle, min_max_var: c_int) -> c_int;
         pub fn ccadical_propagations(solver: *mut CaDiCaLHandle) -> i64;
         pub fn ccadical_decisions(solver: *mut CaDiCaLHandle) -> i64;
         pub fn ccadical_conflicts(solver: *mut CaDiCaLHandle) -> i64;
     }
 
     // >= v1.5.4
-    #[cfg(any(
-        feature = "v1-5-4",
-        feature = "v1-5-5",
-        feature = "v1-5-6",
-        feature = "v1-6-0",
-        feature = "v1-7-0",
-        all(
-            not(feature = "v1-5-3"),
-            not(feature = "v1-5-2"),
-            not(feature = "v1-5-1"),
-            not(feature = "v1-5-0")
-        )
+    #[cfg(all(
+        not(feature = "v1-5-3"),
+        not(feature = "v1-5-2"),
+        not(feature = "v1-5-1"),
+        not(feature = "v1-5-0")
     ))]
     #[link(name = "cadical", kind = "static")]
     extern "C" {
diff --git a/capi/build.rs b/capi/build.rs
index 7fd6a694..75c47ecb 100644
--- a/capi/build.rs
+++ b/capi/build.rs
@@ -27,11 +27,8 @@ fn main() {
     // Setup inline-c
     let include_dir = env::var("CARGO_MANIFEST_DIR").unwrap();
     let ld_dir = target_dir().unwrap();
-    #[cfg(feature = "pyapi")]
-    let python_lib = pyo3_build_config::get().lib_name.as_ref().unwrap();
 
     let cflags = format!("cargo:rustc-env=INLINE_C_RS_CFLAGS=-I{I} -L{L} -lrustsat_capi -D_DEBUG -D_CRT_SECURE_NO_WARNINGS", I=include_dir, L=ld_dir.to_string_lossy());
-    #[cfg(feature = "compression")]
     let cflags = format!("{} -llzma -lbz2", cflags);
     println!("{}", cflags);
 
@@ -39,7 +36,6 @@ fn main() {
         "cargo:rustc-env=INLINE_C_RS_LDFLAGS={L}/librustsat_capi.a",
         L = ld_dir.to_string_lossy()
     );
-    #[cfg(feature = "compression")]
     let ldflags = format!("{} -llzma -lbz2", ldflags);
     println!("{}", ldflags);
 }
diff --git a/capi/src/lib.rs b/capi/src/lib.rs
index 095fcb7d..e92904b0 100644
--- a/capi/src/lib.rs
+++ b/capi/src/lib.rs
@@ -63,6 +63,25 @@ pub mod encodings {
         fn n_clauses(&self) -> usize {
             self.n_clauses
         }
+
+        fn extend_clauses<T>(&mut self, cl_iter: T) -> Result<(), rustsat::OutOfMemory>
+        where
+            T: IntoIterator<Item = Clause>,
+        {
+            cl_iter.into_iter().for_each(|cl| {
+                cl.into_iter()
+                    .for_each(|l| (self.ccol)(l.to_ipasir(), self.cdata));
+                (self.ccol)(0, self.cdata);
+            });
+            Ok(())
+        }
+
+        fn add_clause(&mut self, cl: Clause) -> Result<(), rustsat::OutOfMemory> {
+            cl.into_iter()
+                .for_each(|l| (self.ccol)(l.to_ipasir(), self.cdata));
+            (self.ccol)(0, self.cdata);
+            Ok(())
+        }
     }
 
     impl Extend<Clause> for ClauseCollector {
@@ -186,7 +205,9 @@ pub mod encodings {
             let mut collector = ClauseCollector::new(collector, collector_data);
             let mut var_manager = VarManager::new(n_vars_used);
             let mut boxed = unsafe { Box::from_raw(tot) };
-            boxed.encode_ub_change(min_bound..=max_bound, &mut collector, &mut var_manager);
+            boxed
+                .encode_ub_change(min_bound..=max_bound, &mut collector, &mut var_manager)
+                .expect("clause collector returned out of memory");
             Box::into_raw(boxed);
         }
 
@@ -358,7 +379,9 @@ pub mod encodings {
             let mut collector = ClauseCollector::new(collector, collector_data);
             let mut var_manager = VarManager::new(n_vars_used);
             let mut boxed = unsafe { Box::from_raw(dpw) };
-            boxed.encode_ub_change(min_bound..=max_bound, &mut collector, &mut var_manager);
+            boxed
+                .encode_ub_change(min_bound..=max_bound, &mut collector, &mut var_manager)
+                .expect("clause collector returned out of memory");
             Box::into_raw(boxed);
         }
 
diff --git a/docs/0-5-0-migration-guide.md b/docs/0-5-0-migration-guide.md
index c7203dab..89f49e3b 100644
--- a/docs/0-5-0-migration-guide.md
+++ b/docs/0-5-0-migration-guide.md
@@ -45,3 +45,20 @@ There have been some API changes to improve usability, even though they are brea
 - Methods providing references to internal data are now named `_ref` and `_mut`
   if mutability is allowed. If only a non-mutable accessor is present, the `_ref`
   suffix is omitted (e.g., for `SatInstance::cnf`).
+
+## Handling Out-Of-Memory
+
+This release also includes a push towards catching the most common cases where
+this library could run out of memory. The two main cases of this are adding
+clauses to solvers and generating CNF encodings. For the first, C++ error
+exceptions are now caught in the C-API wrapper and a Rust error
+(`rustsat::OutOfMemory::ExternalApi`) is returned. The other case is if a
+clause collector used when generating an encoding runs out of memory. For this
+reason, the `CollectClauses` trait now does not use Rust's standard `Extend`
+crate any more, but has the functions `extend_clauses` and `add_clause`.
+`CollectClauses` is mainly implemented by `Cnf` and solver (and newly by
+`SatInstance`). In the Rust types, `try_reserve` is now used and
+`rustsat::OutOfMemory::TryReserve` will be returned if memory allocation fails.
+For most use cases, there are at most some more errors that you can treat with
+`unwrap` or `expect` to get the same behaviour as previously. This just enables
+more sophisticated memory error handling now.
diff --git a/glucose/cppsrc b/glucose/cppsrc
index a244a12a..ddb5ef27 160000
--- a/glucose/cppsrc
+++ b/glucose/cppsrc
@@ -1,1 +1,1 @@
-Subproject commit a244a12a3f34da6c93377a6196291494fddf491e
+Subproject commit ddb5ef27286ab6729efb66e201d9aeccc72622a5
diff --git a/glucose/src/core.rs b/glucose/src/core.rs
index ab9b4769..f3d1bbab 100644
--- a/glucose/src/core.rs
+++ b/glucose/src/core.rs
@@ -5,6 +5,8 @@
 
 use core::ffi::{c_int, CStr};
 
+use crate::handle_oom;
+
 use super::{InternalSolverState, InvalidApiReturn, Limit};
 use cpu_time::ProcessTime;
 use ffi::Glucose4Handle;
@@ -27,8 +29,12 @@ unsafe impl Send for Glucose {}
 
 impl Default for Glucose {
     fn default() -> Self {
+        let handle = unsafe { ffi::cglucose4_init() };
+        if handle.is_null() {
+            panic!("not enough memory to initialize glucose solver")
+        }
         Self {
-            handle: unsafe { ffi::cglucose4_init() },
+            handle,
             state: Default::default(),
             stats: Default::default(),
         }
@@ -112,7 +118,7 @@ impl Solve for Glucose {
         }
         let start = ProcessTime::now();
         // Solve with glucose backend
-        let res = unsafe { ffi::cglucose4_solve(self.handle) };
+        let res = handle_oom!(unsafe { ffi::cglucose4_solve(self.handle) });
         self.stats.cpu_solve_time += start.elapsed();
         match res {
             0 => {
@@ -167,10 +173,10 @@ impl Solve for Glucose {
                 / self.stats.n_clauses as f32;
         self.state = InternalSolverState::Input;
         // Call glucose backend
-        clause.iter().for_each(|l| unsafe {
-            ffi::cglucose4_add(self.handle, l.to_ipasir());
-        });
-        unsafe { ffi::cglucose4_add(self.handle, 0) };
+        for l in clause {
+            handle_oom!(unsafe { ffi::cglucose4_add(self.handle, l.to_ipasir()) });
+        }
+        handle_oom!(unsafe { ffi::cglucose4_add(self.handle, 0) });
         Ok(())
     }
 }
@@ -182,7 +188,7 @@ impl SolveIncremental for Glucose {
         for a in assumps {
             unsafe { ffi::cglucose4_assume(self.handle, a.to_ipasir()) }
         }
-        let res = unsafe { ffi::cglucose4_solve(self.handle) };
+        let res = handle_oom!(unsafe { ffi::cglucose4_solve(self.handle) });
         self.stats.cpu_solve_time += start.elapsed();
         match res {
             0 => {
@@ -247,7 +253,7 @@ impl InterruptSolver for Interrupter {
 impl PhaseLit for Glucose {
     /// Forces the default decision phase of a variable to a certain value
     fn phase_lit(&mut self, lit: Lit) -> anyhow::Result<()> {
-        unsafe { ffi::cglucose4_phase(self.handle, lit.to_ipasir()) };
+        handle_oom!(unsafe { ffi::cglucose4_phase(self.handle, lit.to_ipasir()) });
         Ok(())
     }
 
@@ -374,12 +380,12 @@ mod ffi {
         pub fn cglucose4_signature() -> *const c_char;
         pub fn cglucose4_init() -> *mut Glucose4Handle;
         pub fn cglucose4_release(solver: *mut Glucose4Handle);
-        pub fn cglucose4_add(solver: *mut Glucose4Handle, lit_or_zero: c_int);
+        pub fn cglucose4_add(solver: *mut Glucose4Handle, lit_or_zero: c_int) -> c_int;
         pub fn cglucose4_assume(solver: *mut Glucose4Handle, lit: c_int);
         pub fn cglucose4_solve(solver: *mut Glucose4Handle) -> c_int;
         pub fn cglucose4_val(solver: *mut Glucose4Handle, lit: c_int) -> c_int;
         pub fn cglucose4_failed(solver: *mut Glucose4Handle, lit: c_int) -> c_int;
-        pub fn cglucose4_phase(solver: *mut Glucose4Handle, lit: c_int);
+        pub fn cglucose4_phase(solver: *mut Glucose4Handle, lit: c_int) -> c_int;
         pub fn cglucose4_unphase(solver: *mut Glucose4Handle, lit: c_int);
         pub fn cglucose4_n_assigns(solver: *mut Glucose4Handle) -> c_int;
         pub fn cglucose4_n_clauses(solver: *mut Glucose4Handle) -> c_int;
diff --git a/glucose/src/lib.rs b/glucose/src/lib.rs
index 0020227b..4239cca3 100644
--- a/glucose/src/lib.rs
+++ b/glucose/src/lib.rs
@@ -24,6 +24,8 @@ use thiserror::Error;
 pub mod core;
 pub mod simp;
 
+const OUT_OF_MEM: c_int = 50;
+
 /// Fatal error returned if the Glucose API returns an invalid value
 #[derive(Error, Clone, Copy, PartialEq, Eq, Debug)]
 #[error("glucose c-api returned an invalid value: {api_call} -> {value}")]
@@ -80,3 +82,17 @@ impl fmt::Display for Limit {
         }
     }
 }
+
+macro_rules! handle_oom {
+    ($val:expr) => {{
+        let val = $val;
+        if val == crate::OUT_OF_MEM {
+            return anyhow::Context::context(
+                Err(rustsat::OutOfMemory::ExternalApi),
+                "glucose out of memory",
+            );
+        }
+        val
+    }};
+}
+pub(crate) use handle_oom;
diff --git a/glucose/src/simp.rs b/glucose/src/simp.rs
index 84fcee65..d7f14178 100644
--- a/glucose/src/simp.rs
+++ b/glucose/src/simp.rs
@@ -5,6 +5,8 @@
 
 use core::ffi::{c_int, CStr};
 
+use crate::handle_oom;
+
 use super::{AssumpEliminated, InternalSolverState, InvalidApiReturn, Limit};
 use cpu_time::ProcessTime;
 use ffi::Glucose4Handle;
@@ -28,8 +30,12 @@ unsafe impl Send for Glucose {}
 
 impl Default for Glucose {
     fn default() -> Self {
+        let handle = unsafe { ffi::cglucosesimp4_init() };
+        if handle.is_null() {
+            panic!("not enough memory to initialize glucose solver")
+        }
         Self {
-            handle: unsafe { ffi::cglucosesimp4_init() },
+            handle,
             state: Default::default(),
             stats: Default::default(),
         }
@@ -120,7 +126,7 @@ impl Solve for Glucose {
         }
         let start = ProcessTime::now();
         // Solve with glucose backend
-        let res = unsafe { ffi::cglucosesimp4_solve(self.handle) };
+        let res = handle_oom!(unsafe { ffi::cglucosesimp4_solve(self.handle) });
         self.stats.cpu_solve_time += start.elapsed();
         match res {
             0 => {
@@ -175,10 +181,10 @@ impl Solve for Glucose {
                 / self.stats.n_clauses as f32;
         self.state = InternalSolverState::Input;
         // Call glucose backend
-        clause.iter().for_each(|l| unsafe {
-            ffi::cglucosesimp4_add(self.handle, l.to_ipasir());
-        });
-        unsafe { ffi::cglucosesimp4_add(self.handle, 0) };
+        for l in clause {
+            handle_oom!(unsafe { ffi::cglucosesimp4_add(self.handle, l.to_ipasir()) });
+        }
+        handle_oom!(unsafe { ffi::cglucosesimp4_add(self.handle, 0) });
         Ok(())
     }
 }
@@ -195,7 +201,7 @@ impl SolveIncremental for Glucose {
         for a in assumps {
             unsafe { ffi::cglucosesimp4_assume(self.handle, a.to_ipasir()) }
         }
-        let res = unsafe { ffi::cglucosesimp4_solve(self.handle) };
+        let res = handle_oom!(unsafe { ffi::cglucosesimp4_solve(self.handle) });
         self.stats.cpu_solve_time += start.elapsed();
         match res {
             0 => {
@@ -260,7 +266,7 @@ impl InterruptSolver for Interrupter {
 impl PhaseLit for Glucose {
     /// Forces the default decision phase of a variable to a certain value
     fn phase_lit(&mut self, lit: Lit) -> anyhow::Result<()> {
-        unsafe { ffi::cglucosesimp4_phase(self.handle, lit.to_ipasir()) };
+        handle_oom!(unsafe { ffi::cglucosesimp4_phase(self.handle, lit.to_ipasir()) });
         Ok(())
     }
 
@@ -404,12 +410,12 @@ mod ffi {
         pub fn cglucose4_signature() -> *const c_char;
         pub fn cglucosesimp4_init() -> *mut Glucose4Handle;
         pub fn cglucosesimp4_release(solver: *mut Glucose4Handle);
-        pub fn cglucosesimp4_add(solver: *mut Glucose4Handle, lit_or_zero: c_int);
+        pub fn cglucosesimp4_add(solver: *mut Glucose4Handle, lit_or_zero: c_int) -> c_int;
         pub fn cglucosesimp4_assume(solver: *mut Glucose4Handle, lit: c_int);
         pub fn cglucosesimp4_solve(solver: *mut Glucose4Handle) -> c_int;
         pub fn cglucosesimp4_val(solver: *mut Glucose4Handle, lit: c_int) -> c_int;
         pub fn cglucosesimp4_failed(solver: *mut Glucose4Handle, lit: c_int) -> c_int;
-        pub fn cglucosesimp4_phase(solver: *mut Glucose4Handle, lit: c_int);
+        pub fn cglucosesimp4_phase(solver: *mut Glucose4Handle, lit: c_int) -> c_int;
         pub fn cglucosesimp4_unphase(solver: *mut Glucose4Handle, lit: c_int);
         pub fn cglucosesimp4_n_assigns(solver: *mut Glucose4Handle) -> c_int;
         pub fn cglucosesimp4_n_clauses(solver: *mut Glucose4Handle) -> c_int;
diff --git a/kissat/Cargo.toml b/kissat/Cargo.toml
index b40c0074..beaae3ed 100644
--- a/kissat/Cargo.toml
+++ b/kissat/Cargo.toml
@@ -38,3 +38,5 @@ chrono = "0.4.31"
 
 [dev-dependencies]
 rustsat-solvertests = { path = "../solvertests" }
+clap = { version = "4.5.4", features = ["derive"] }
+signal-hook = { version = "0.3.17" }
diff --git a/kissat/examples/kissat-cli.rs b/kissat/examples/kissat-cli.rs
new file mode 100644
index 00000000..a8c26084
--- /dev/null
+++ b/kissat/examples/kissat-cli.rs
@@ -0,0 +1,135 @@
+//! # CaDiCaL CLI Tool
+//!
+//! A simple CLI wrapper around the CaDiCaL solver Rust interface. This is just an example, if you
+//! want to use CaDiCaL from the CLI, compile the binary from the C++ source directly.
+
+use std::{
+    io,
+    path::{Path, PathBuf},
+    thread,
+};
+
+use anyhow::Context;
+use clap::Parser;
+use rustsat::{
+    instances::{fio::opb, ManageVars, SatInstance},
+    solvers::{Interrupt, InterruptSolver, Solve, SolveStats, SolverResult},
+};
+use rustsat_kissat::Kissat;
+
+enum FileType {
+    Cnf,
+    Opb,
+}
+
+#[derive(Parser)]
+#[command(author, version, about, long_about = None)]
+struct Args {
+    /// The DIMACS CNF input file. Reads from `stdin` if not given.
+    in_path: Option<PathBuf>,
+    /// Parse the input as an OPB file by default
+    #[arg(short, long)]
+    opb: bool,
+}
+
+fn main() -> anyhow::Result<()> {
+    let args = Args::parse();
+
+    let inst: SatInstance = if let Some(in_path) = args.in_path {
+        match determine_file_type(&in_path, args.opb) {
+            FileType::Cnf => SatInstance::from_dimacs_path(in_path)
+                .context("error parsing the input file as CNF")?,
+            FileType::Opb => SatInstance::from_opb_path(in_path, opb::Options::default())
+                .context("error parsing the input file as OPB")?,
+        }
+    } else if args.opb {
+        SatInstance::from_opb(io::BufReader::new(io::stdin()), opb::Options::default())
+            .context("error parsing input as OPB")?
+    } else {
+        SatInstance::from_dimacs(io::BufReader::new(io::stdin()))
+            .context("error parsing input as CNF")?
+    };
+
+    rustsat_kissat::call_instead_of_abort(Some(kissat_abort));
+    solve::<Kissat>(inst)
+}
+
+extern "C" fn kissat_abort() {
+    println!("s UNKNOWN");
+    panic!("kissat called abort");
+}
+
+fn solve<S: Solve + SolveStats + Interrupt + Default>(inst: SatInstance) -> anyhow::Result<()> {
+    let mut solver = S::default();
+
+    #[cfg(not(target_family = "windows"))]
+    {
+        // Setup signal handling
+        let interrupter = solver.interrupter();
+        let mut signals = signal_hook::iterator::Signals::new([
+            signal_hook::consts::SIGTERM,
+            signal_hook::consts::SIGINT,
+            signal_hook::consts::SIGXCPU,
+            signal_hook::consts::SIGABRT,
+        ])?;
+        // Thread for catching incoming signals
+        thread::spawn(move || {
+            for _ in signals.forever() {
+                interrupter.interrupt();
+            }
+        });
+    }
+
+    let (cnf, vm) = inst.into_cnf();
+    if let Some(max_var) = vm.max_var() {
+        solver.reserve(max_var)?;
+    }
+    solver.add_cnf(cnf)?;
+    match solver.solve() {
+        Err(err) => {
+            println!("s UNKNOWN");
+            return Err(err);
+        }
+        Ok(res) => match res {
+            SolverResult::Sat => {
+                println!("s SATISFIABLE");
+                println!("v {}", solver.full_solution()?);
+            }
+            SolverResult::Unsat => println!("s UNSATISFIABLE"),
+            SolverResult::Interrupted => println!("s UNKNOWN"),
+        },
+    };
+    Ok(())
+}
+
+macro_rules! is_one_of {
+    ($a:expr, $($b:expr),*) => {
+        $( $a == $b || )* false
+    }
+}
+
+fn determine_file_type(in_path: &Path, opb_default: bool) -> FileType {
+    if let Some(ext) = in_path.extension() {
+        let path_without_compr = in_path.with_extension("");
+        let ext = if is_one_of!(ext, "gz", "bz2") {
+            // Strip compression extension
+            match path_without_compr.extension() {
+                Some(ext) => ext,
+                None => return FileType::Cnf, // Fallback default
+            }
+        } else {
+            ext
+        };
+        if "opb" == ext {
+            return FileType::Opb;
+        };
+        if "cnf" == ext {
+            return FileType::Cnf;
+        }
+    };
+    if opb_default {
+        FileType::Opb
+    } else {
+        FileType::Cnf
+    } // Fallback default
+}
diff --git a/kissat/src/lib.rs b/kissat/src/lib.rs
index 818ab5ea..145b7668 100644
--- a/kissat/src/lib.rs
+++ b/kissat/src/lib.rs
@@ -434,6 +434,20 @@ impl fmt::Display for Limit {
     }
 }
 
+extern "C" fn panic_instead_of_abort() {
+    panic!("kissat called kissat_abort");
+}
+
+/// Changes Kissat's abort behaviour to cause a Rust panic instead
+pub fn panic_intead_of_abort() {
+    unsafe { ffi::kissat_call_function_instead_of_abort(Some(panic_instead_of_abort)) };
+}
+
+/// Changes Kissat's abort behaviour to call the given function instead
+pub fn call_instead_of_abort(abort: Option<extern "C" fn()>) {
+    unsafe { ffi::kissat_call_function_instead_of_abort(abort) };
+}
+
 #[cfg(test)]
 mod test {
     use super::{Config, Kissat, Limit};
@@ -516,6 +530,8 @@ mod ffi {
         pub fn kissat_set_conflict_limit(solver: *mut KissatHandle, limit: c_uint);
         pub fn kissat_set_decision_limit(solver: *mut KissatHandle, limit: c_uint);
         pub fn kissat_print_statistics(solver: *mut KissatHandle);
+        // This is from `error.h`
+        pub fn kissat_call_function_instead_of_abort(abort: Option<extern "C" fn()>);
     }
 
     // Raw callbacks forwarding to user callbacks
diff --git a/minisat/Cargo.toml b/minisat/Cargo.toml
index ebae177f..314f5f3d 100644
--- a/minisat/Cargo.toml
+++ b/minisat/Cargo.toml
@@ -33,3 +33,5 @@ cmake = "0.1.50"
 
 [dev-dependencies]
 rustsat-solvertests = { path = "../solvertests" }
+clap = { version = "4.5.4", features = ["derive"] }
+signal-hook = { version = "0.3.17" }
diff --git a/minisat/cppsrc b/minisat/cppsrc
index e168f6e7..c17b905d 160000
--- a/minisat/cppsrc
+++ b/minisat/cppsrc
@@ -1,1 +1,1 @@
-Subproject commit e168f6e72600f4b04769b0f3bbb7f89b1a200a67
+Subproject commit c17b905d3654cdfffe5837cf275402e4f40c3435
diff --git a/minisat/examples/minisat-cli.rs b/minisat/examples/minisat-cli.rs
new file mode 100644
index 00000000..48ccc23e
--- /dev/null
+++ b/minisat/examples/minisat-cli.rs
@@ -0,0 +1,136 @@
+//! # Minisat CLI Tool
+//!
+//! A simple CLI wrapper around the MiniSAT solver Rust interface. This is just an example, if you
+//! want to use MiniSAT from the CLI, compile the binary from the C++ source directly.
+
+use std::{
+    io,
+    path::{Path, PathBuf},
+    thread,
+};
+
+use anyhow::Context;
+use clap::Parser;
+use rustsat::{
+    instances::{fio::opb, ManageVars, SatInstance},
+    solvers::{Interrupt, InterruptSolver, Solve, SolveStats, SolverResult},
+};
+use rustsat_minisat::{core, simp};
+
+enum FileType {
+    Cnf,
+    Opb,
+}
+
+#[derive(Parser)]
+#[command(author, version, about, long_about = None)]
+struct Args {
+    /// The DIMACS CNF input file. Reads from `stdin` if not given.
+    in_path: Option<PathBuf>,
+    /// Use the version of MiniSAT with preprocessing
+    #[arg(short, long)]
+    simp: bool,
+    /// Parse the input as an OPB file by default
+    #[arg(short, long)]
+    opb: bool,
+}
+
+fn main() -> anyhow::Result<()> {
+    let args = Args::parse();
+
+    let inst: SatInstance = if let Some(in_path) = args.in_path {
+        match determine_file_type(&in_path, args.opb) {
+            FileType::Cnf => SatInstance::from_dimacs_path(in_path)
+                .context("error parsing the input file as CNF")?,
+            FileType::Opb => SatInstance::from_opb_path(in_path, opb::Options::default())
+                .context("error parsing the input file as OPB")?,
+        }
+    } else if args.opb {
+        SatInstance::from_opb(io::BufReader::new(io::stdin()), opb::Options::default())
+            .context("error parsing input as OPB")?
+    } else {
+        SatInstance::from_dimacs(io::BufReader::new(io::stdin()))
+            .context("error parsing input as CNF")?
+    };
+
+    if args.simp {
+        solve::<simp::Minisat>(inst)
+    } else {
+        solve::<core::Minisat>(inst)
+    }
+}
+
+fn solve<S: Solve + SolveStats + Interrupt + Default>(inst: SatInstance) -> anyhow::Result<()> {
+    let mut solver = S::default();
+
+    #[cfg(not(target_family = "windows"))]
+    {
+        // Setup signal handling
+        let interrupter = solver.interrupter();
+        let mut signals = signal_hook::iterator::Signals::new([
+            signal_hook::consts::SIGTERM,
+            signal_hook::consts::SIGINT,
+            signal_hook::consts::SIGXCPU,
+            signal_hook::consts::SIGABRT,
+        ])?;
+        // Thread for catching incoming signals
+        thread::spawn(move || {
+            for _ in signals.forever() {
+                interrupter.interrupt();
+            }
+        });
+    }
+
+    let (cnf, vm) = inst.into_cnf();
+    if let Some(max_var) = vm.max_var() {
+        solver.reserve(max_var)?;
+    }
+    solver.add_cnf(cnf)?;
+    match solver.solve() {
+        Err(err) => {
+            println!("s UNKNOWN");
+            return Err(err);
+        }
+        Ok(res) => match res {
+            SolverResult::Sat => {
+                println!("s SATISFIABLE");
+                println!("v {}", solver.full_solution()?);
+            }
+            SolverResult::Unsat => println!("s UNSATISFIABLE"),
+            SolverResult::Interrupted => println!("s UNKNOWN"),
+        },
+    };
+    Ok(())
+}
+
+macro_rules! is_one_of {
+    ($a:expr, $($b:expr),*) => {
+        $( $a == $b || )* false
+    }
+}
+
+fn determine_file_type(in_path: &Path, opb_default: bool) -> FileType {
+    if let Some(ext) = in_path.extension() {
+        let path_without_compr = in_path.with_extension("");
+        let ext = if is_one_of!(ext, "gz", "bz2") {
+            // Strip compression extension
+            match path_without_compr.extension() {
+                Some(ext) => ext,
+                None => return FileType::Cnf, // Fallback default
+            }
+        } else {
+            ext
+        };
+        if "opb" == ext {
+            return FileType::Opb;
+        };
+        if "cnf" == ext {
+            return FileType::Cnf;
+        }
+    };
+    if opb_default {
+        FileType::Opb
+    } else {
+        FileType::Cnf
+    } // Fallback default
+}
diff --git a/minisat/src/core.rs b/minisat/src/core.rs
index 5d1200b4..c90fe3c8 100644
--- a/minisat/src/core.rs
+++ b/minisat/src/core.rs
@@ -5,7 +5,7 @@
 
 use core::ffi::{c_int, CStr};
 
-use super::{InternalSolverState, InvalidApiReturn, Limit};
+use super::{handle_oom, InternalSolverState, InvalidApiReturn, Limit};
 use cpu_time::ProcessTime;
 use ffi::MinisatHandle;
 use rustsat::{
@@ -27,8 +27,12 @@ unsafe impl Send for Minisat {}
 
 impl Default for Minisat {
     fn default() -> Self {
+        let handle = unsafe { ffi::cminisat_init() };
+        if handle.is_null() {
+            panic!("not enough memory to initialize minisat solver")
+        }
         Self {
-            handle: unsafe { ffi::cminisat_init() },
+            handle,
             state: Default::default(),
             stats: Default::default(),
         }
@@ -112,7 +116,7 @@ impl Solve for Minisat {
         }
         let start = ProcessTime::now();
         // Solve with minisat backend
-        let res = unsafe { ffi::cminisat_solve(self.handle) };
+        let res = handle_oom!(unsafe { ffi::cminisat_solve(self.handle) });
         self.stats.cpu_solve_time += start.elapsed();
         match res {
             0 => {
@@ -167,10 +171,10 @@ impl Solve for Minisat {
                 / self.stats.n_clauses as f32;
         self.state = InternalSolverState::Input;
         // Call minisat backend
-        clause.iter().for_each(|l| unsafe {
-            ffi::cminisat_add(self.handle, l.to_ipasir());
-        });
-        unsafe { ffi::cminisat_add(self.handle, 0) };
+        for l in clause {
+            handle_oom!(unsafe { ffi::cminisat_add(self.handle, l.to_ipasir()) });
+        }
+        handle_oom!(unsafe { ffi::cminisat_add(self.handle, 0) });
         Ok(())
     }
 }
@@ -182,7 +186,7 @@ impl SolveIncremental for Minisat {
         for a in assumps {
             unsafe { ffi::cminisat_assume(self.handle, a.to_ipasir()) }
         }
-        let res = unsafe { ffi::cminisat_solve(self.handle) };
+        let res = handle_oom!(unsafe { ffi::cminisat_solve(self.handle) });
         self.stats.cpu_solve_time += start.elapsed();
         match res {
             0 => {
@@ -247,7 +251,7 @@ impl InterruptSolver for Interrupter {
 impl PhaseLit for Minisat {
     /// Forces the default decision phase of a variable to a certain value
     fn phase_lit(&mut self, lit: Lit) -> anyhow::Result<()> {
-        unsafe { ffi::cminisat_phase(self.handle, lit.to_ipasir()) };
+        handle_oom!(unsafe { ffi::cminisat_phase(self.handle, lit.to_ipasir()) });
         Ok(())
     }
 
@@ -373,12 +377,12 @@ mod ffi {
         pub fn cminisat_signature() -> *const c_char;
         pub fn cminisat_init() -> *mut MinisatHandle;
         pub fn cminisat_release(solver: *mut MinisatHandle);
-        pub fn cminisat_add(solver: *mut MinisatHandle, lit_or_zero: c_int);
+        pub fn cminisat_add(solver: *mut MinisatHandle, lit_or_zero: c_int) -> c_int;
         pub fn cminisat_assume(solver: *mut MinisatHandle, lit: c_int);
         pub fn cminisat_solve(solver: *mut MinisatHandle) -> c_int;
         pub fn cminisat_val(solver: *mut MinisatHandle, lit: c_int) -> c_int;
         pub fn cminisat_failed(solver: *mut MinisatHandle, lit: c_int) -> c_int;
-        pub fn cminisat_phase(solver: *mut MinisatHandle, lit: c_int);
+        pub fn cminisat_phase(solver: *mut MinisatHandle, lit: c_int) -> c_int;
         pub fn cminisat_unphase(solver: *mut MinisatHandle, lit: c_int);
         pub fn cminisat_n_assigns(solver: *mut MinisatHandle) -> c_int;
         pub fn cminisat_n_clauses(solver: *mut MinisatHandle) -> c_int;
diff --git a/minisat/src/lib.rs b/minisat/src/lib.rs
index 1fb1f2be..93c36019 100644
--- a/minisat/src/lib.rs
+++ b/minisat/src/lib.rs
@@ -24,6 +24,8 @@ use thiserror::Error;
 pub mod core;
 pub mod simp;
 
+const OUT_OF_MEM: c_int = 50;
+
 /// Fatal error returned if the Minisat API returns an invalid value
 #[derive(Error, Clone, Copy, PartialEq, Eq, Debug)]
 #[error("minisat c-api returned an invalid value: {api_call} -> {value}")]
@@ -80,3 +82,17 @@ impl fmt::Display for Limit {
         }
     }
 }
+
+macro_rules! handle_oom {
+    ($val:expr) => {{
+        let val = $val;
+        if val == crate::OUT_OF_MEM {
+            return anyhow::Context::context(
+                Err(rustsat::OutOfMemory::ExternalApi),
+                "minisat out of memory",
+            );
+        }
+        val
+    }};
+}
+pub(crate) use handle_oom;
diff --git a/minisat/src/simp.rs b/minisat/src/simp.rs
index 8c56b86b..9a540365 100644
--- a/minisat/src/simp.rs
+++ b/minisat/src/simp.rs
@@ -5,7 +5,7 @@
 
 use core::ffi::{c_int, CStr};
 
-use super::{AssumpEliminated, InternalSolverState, InvalidApiReturn, Limit};
+use super::{handle_oom, AssumpEliminated, InternalSolverState, InvalidApiReturn, Limit};
 use cpu_time::ProcessTime;
 use ffi::MinisatHandle;
 use rustsat::{
@@ -28,8 +28,12 @@ unsafe impl Send for Minisat {}
 
 impl Default for Minisat {
     fn default() -> Self {
+        let handle = unsafe { ffi::cminisatsimp_init() };
+        if handle.is_null() {
+            panic!("not enough memory to initialize minisat solver")
+        }
         Self {
-            handle: unsafe { ffi::cminisatsimp_init() },
+            handle,
             state: Default::default(),
             stats: Default::default(),
         }
@@ -120,7 +124,7 @@ impl Solve for Minisat {
         }
         let start = ProcessTime::now();
         // Solve with minisat backend
-        let res = unsafe { ffi::cminisatsimp_solve(self.handle) };
+        let res = handle_oom!(unsafe { ffi::cminisatsimp_solve(self.handle) });
         self.stats.cpu_solve_time += start.elapsed();
         match res {
             0 => {
@@ -175,10 +179,10 @@ impl Solve for Minisat {
                 / self.stats.n_clauses as f32;
         self.state = InternalSolverState::Input;
         // Call minisat backend
-        clause.iter().for_each(|l| unsafe {
-            ffi::cminisatsimp_add(self.handle, l.to_ipasir());
-        });
-        unsafe { ffi::cminisatsimp_add(self.handle, 0) };
+        for l in clause {
+            handle_oom!(unsafe { ffi::cminisatsimp_add(self.handle, l.to_ipasir()) });
+        }
+        handle_oom!(unsafe { ffi::cminisatsimp_add(self.handle, 0) });
         Ok(())
     }
 }
@@ -195,7 +199,7 @@ impl SolveIncremental for Minisat {
         for a in assumps {
             unsafe { ffi::cminisatsimp_assume(self.handle, a.to_ipasir()) }
         }
-        let res = unsafe { ffi::cminisatsimp_solve(self.handle) };
+        let res = handle_oom!(unsafe { ffi::cminisatsimp_solve(self.handle) });
         self.stats.cpu_solve_time += start.elapsed();
         match res {
             0 => {
@@ -260,7 +264,7 @@ impl InterruptSolver for Interrupter {
 impl PhaseLit for Minisat {
     /// Forces the default decision phase of a variable to a certain value
     fn phase_lit(&mut self, lit: Lit) -> anyhow::Result<()> {
-        unsafe { ffi::cminisatsimp_phase(self.handle, lit.to_ipasir()) };
+        handle_oom!(unsafe { ffi::cminisatsimp_phase(self.handle, lit.to_ipasir()) });
         Ok(())
     }
 
@@ -405,12 +409,12 @@ mod ffi {
         pub fn cminisat_signature() -> *const c_char;
         pub fn cminisatsimp_init() -> *mut MinisatHandle;
         pub fn cminisatsimp_release(solver: *mut MinisatHandle);
-        pub fn cminisatsimp_add(solver: *mut MinisatHandle, lit_or_zero: c_int);
+        pub fn cminisatsimp_add(solver: *mut MinisatHandle, lit_or_zero: c_int) -> c_int;
         pub fn cminisatsimp_assume(solver: *mut MinisatHandle, lit: c_int);
         pub fn cminisatsimp_solve(solver: *mut MinisatHandle) -> c_int;
         pub fn cminisatsimp_val(solver: *mut MinisatHandle, lit: c_int) -> c_int;
         pub fn cminisatsimp_failed(solver: *mut MinisatHandle, lit: c_int) -> c_int;
-        pub fn cminisatsimp_phase(solver: *mut MinisatHandle, lit: c_int);
+        pub fn cminisatsimp_phase(solver: *mut MinisatHandle, lit: c_int) -> c_int;
         pub fn cminisatsimp_unphase(solver: *mut MinisatHandle, lit: c_int);
         pub fn cminisatsimp_n_assigns(solver: *mut MinisatHandle) -> c_int;
         pub fn cminisatsimp_n_clauses(solver: *mut MinisatHandle) -> c_int;
diff --git a/pyapi/src/encodings.rs b/pyapi/src/encodings.rs
index e7f1bba4..b5563651 100644
--- a/pyapi/src/encodings.rs
+++ b/pyapi/src/encodings.rs
@@ -19,6 +19,7 @@ use rustsat::{
 };
 
 use crate::{
+    handle_oom,
     instances::{Cnf, VarManager},
     types::Lit,
 };
@@ -89,12 +90,18 @@ impl Totalizer {
     /// Incrementally builds the totalizer encoding to that upper bounds
     /// in the range `max_ub..=min_ub` can be enforced. New variables will
     /// be taken from `var_manager`.
-    fn encode_ub(&mut self, max_ub: usize, min_ub: usize, var_manager: &mut VarManager) -> Cnf {
+    fn encode_ub(
+        &mut self,
+        max_ub: usize,
+        min_ub: usize,
+        var_manager: &mut VarManager,
+    ) -> PyResult<Cnf> {
         let mut cnf = RsCnf::new();
         let var_manager: &mut BasicVarManager = var_manager.into();
-        self.0
-            .encode_ub_change(max_ub..=min_ub, &mut cnf, var_manager);
-        cnf.into()
+        handle_oom!(self
+            .0
+            .encode_ub_change(max_ub..=min_ub, &mut cnf, var_manager));
+        Ok(cnf.into())
     }
 
     /// Gets assumptions to enforce the given upper bound. Make sure that
@@ -165,12 +172,18 @@ impl GeneralizedTotalizer {
     /// Incrementally builds the GTE encoding to that upper bounds
     /// in the range `max_ub..=min_ub` can be enforced. New variables will
     /// be taken from `var_manager`.
-    fn encode_ub(&mut self, max_ub: usize, min_ub: usize, var_manager: &mut VarManager) -> Cnf {
+    fn encode_ub(
+        &mut self,
+        max_ub: usize,
+        min_ub: usize,
+        var_manager: &mut VarManager,
+    ) -> PyResult<Cnf> {
         let mut cnf = RsCnf::new();
         let var_manager: &mut BasicVarManager = var_manager.into();
-        self.0
-            .encode_ub_change(max_ub..=min_ub, &mut cnf, var_manager);
-        cnf.into()
+        handle_oom!(self
+            .0
+            .encode_ub_change(max_ub..=min_ub, &mut cnf, var_manager));
+        Ok(cnf.into())
     }
 
     /// Gets assumptions to enforce the given upper bound. Make sure that
@@ -235,12 +248,18 @@ impl DynamicPolyWatchdog {
     /// Incrementally builds the DPW encoding to that upper bounds
     /// in the range `max_ub..=min_ub` can be enforced. New variables will
     /// be taken from `var_manager`.
-    fn encode_ub(&mut self, max_ub: usize, min_ub: usize, var_manager: &mut VarManager) -> Cnf {
+    fn encode_ub(
+        &mut self,
+        max_ub: usize,
+        min_ub: usize,
+        var_manager: &mut VarManager,
+    ) -> PyResult<Cnf> {
         let mut cnf = RsCnf::new();
         let var_manager: &mut BasicVarManager = var_manager.into();
-        self.0
-            .encode_ub_change(max_ub..=min_ub, &mut cnf, var_manager);
-        cnf.into()
+        handle_oom!(self
+            .0
+            .encode_ub_change(max_ub..=min_ub, &mut cnf, var_manager));
+        Ok(cnf.into())
     }
 
     /// Gets assumptions to enforce the given upper bound. Make sure that
diff --git a/pyapi/src/lib.rs b/pyapi/src/lib.rs
index 3ef13937..6cf1f0a3 100644
--- a/pyapi/src/lib.rs
+++ b/pyapi/src/lib.rs
@@ -70,3 +70,13 @@ fn rustsat(py: Python<'_>, m: &Bound<'_, PyModule>) -> PyResult<()> {
 
     Ok(())
 }
+
+macro_rules! handle_oom {
+    ($result:expr) => {{
+        match $result {
+            Ok(val) => val,
+            Err(err) => return Err(pyo3::exceptions::PyMemoryError::new_err(format!("{}", err))),
+        }
+    }};
+}
+pub(crate) use handle_oom;
diff --git a/rustsat/examples/profiling.rs b/rustsat/examples/profiling.rs
index 0cb4f122..954065fd 100644
--- a/rustsat/examples/profiling.rs
+++ b/rustsat/examples/profiling.rs
@@ -73,7 +73,7 @@ fn build_full_ub<PBE: BoundUpper + FromIterator<(Lit, usize)>>(lits: &[(Lit, usi
     let mut var_manager = BasicVarManager::default();
     var_manager.increase_next_free(max_var + 1);
     let mut collector = Cnf::new();
-    enc.encode_ub(.., &mut collector, &mut var_manager);
+    enc.encode_ub(.., &mut collector, &mut var_manager).unwrap();
 }
 
 fn main() {
diff --git a/rustsat/src/encodings.rs b/rustsat/src/encodings.rs
index a30056aa..6433728b 100644
--- a/rustsat/src/encodings.rs
+++ b/rustsat/src/encodings.rs
@@ -4,7 +4,7 @@
 
 use thiserror::Error;
 
-use crate::types::Lit;
+use crate::types::{Clause, Lit};
 
 pub mod am1;
 pub mod atomics;
@@ -13,9 +13,21 @@ pub mod pb;
 
 /// Trait for collecting clauses. Mainly used when generating encodings and implemented by
 /// [`crate::instances::Cnf`], and solvers.
-pub trait CollectClauses: Extend<crate::types::Clause> {
+pub trait CollectClauses {
     /// Gets the number of clauses in the collection
     fn n_clauses(&self) -> usize;
+    /// Extends the clause collector with an iterator of clauses
+    ///
+    /// # Error
+    ///
+    /// If the collector runs out of memory, return an [`crate::OutOfMemory`] error.
+    fn extend_clauses<T>(&mut self, cl_iter: T) -> Result<(), crate::OutOfMemory>
+    where
+        T: IntoIterator<Item = Clause>;
+    /// Adds one clause to the collector
+    fn add_clause(&mut self, cl: Clause) -> Result<(), crate::OutOfMemory> {
+        self.extend_clauses([cl])
+    }
 }
 
 /// Errors from encodings
diff --git a/rustsat/src/encodings/am1.rs b/rustsat/src/encodings/am1.rs
index 63648aa4..1190e021 100644
--- a/rustsat/src/encodings/am1.rs
+++ b/rustsat/src/encodings/am1.rs
@@ -20,7 +20,7 @@
 //! enc.encode(&mut encoding, &mut var_manager).unwrap();
 //! ```
 
-use super::{CollectClauses, Error};
+use super::CollectClauses;
 use crate::instances::ManageVars;
 
 mod pairwise;
@@ -35,7 +35,7 @@ pub trait Encode {
         &mut self,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) -> Result<(), Error>
+    ) -> Result<(), crate::OutOfMemory>
     where
         Col: CollectClauses;
 }
diff --git a/rustsat/src/encodings/am1/pairwise.rs b/rustsat/src/encodings/am1/pairwise.rs
index e4513a56..dac0efb0 100644
--- a/rustsat/src/encodings/am1/pairwise.rs
+++ b/rustsat/src/encodings/am1/pairwise.rs
@@ -7,7 +7,7 @@
 use super::Encode;
 use crate::{
     clause,
-    encodings::{CollectClauses, EncodeStats, Error, IterInputs},
+    encodings::{CollectClauses, EncodeStats, IterInputs},
     instances::ManageVars,
     types::Lit,
 };
@@ -34,7 +34,7 @@ impl Encode for Pairwise {
         &mut self,
         collector: &mut Col,
         _var_manager: &mut dyn ManageVars,
-    ) -> Result<(), Error>
+    ) -> Result<(), crate::OutOfMemory>
     where
         Col: CollectClauses,
     {
@@ -43,7 +43,7 @@ impl Encode for Pairwise {
         let clause_iter = (0..self.in_lits.len()).flat_map(|first| {
             (first + 1..self.in_lits.len()).map(move |second| clause![!lits[first], !lits[second]])
         });
-        collector.extend(clause_iter);
+        collector.extend_clauses(clause_iter)?;
         self.n_clauses = collector.n_clauses() - prev_clauses;
         Ok(())
     }
diff --git a/rustsat/src/encodings/card.rs b/rustsat/src/encodings/card.rs
index 9ba9f4d9..a0825641 100644
--- a/rustsat/src/encodings/card.rs
+++ b/rustsat/src/encodings/card.rs
@@ -67,7 +67,8 @@ pub trait BoundUpper: Encode {
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>;
     /// Returns assumptions/units for enforcing an upper bound (`sum of lits <=
@@ -76,24 +77,28 @@ pub trait BoundUpper: Encode {
     /// [`Error::NotEncoded`] will be returned.
     fn enforce_ub(&self, ub: usize) -> Result<Vec<Lit>, Error>;
     /// Encodes an upper bound cardinality constraint to CNF
+    ///
+    /// # Errors
+    ///
+    /// Either an [`Error`] of [`crate::OutOfMemory`]
     fn encode_ub_constr<Col>(
         constr: CardUBConstr,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) -> Result<(), Error>
+    ) -> anyhow::Result<()>
     where
         Col: CollectClauses,
         Self: FromIterator<Lit> + Sized,
     {
         let (lits, ub) = constr.decompose();
         let mut enc = Self::from_iter(lits);
-        enc.encode_ub(ub..ub + 1, collector, var_manager);
-        collector.extend(
+        enc.encode_ub(ub..ub + 1, collector, var_manager)?;
+        collector.extend_clauses(
             enc.enforce_ub(ub)
                 .unwrap()
                 .into_iter()
                 .map(|unit| clause![unit]),
-        );
+        )?;
         Ok(())
     }
 }
@@ -110,7 +115,8 @@ pub trait BoundLower: Encode {
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>;
     /// Returns assumptions/units for enforcing a lower bound (`sum of lits >=
@@ -121,24 +127,28 @@ pub trait BoundLower: Encode {
     /// returned.
     fn enforce_lb(&self, lb: usize) -> Result<Vec<Lit>, Error>;
     /// Encodes a lower bound cardinality constraint to CNF
+    ///
+    /// # Errors
+    ///
+    /// Either an [`Error`] of [`crate::OutOfMemory`]
     fn encode_lb_constr<Col>(
         constr: CardLBConstr,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) -> Result<(), Error>
+    ) -> anyhow::Result<()>
     where
         Col: CollectClauses,
         Self: FromIterator<Lit> + Sized,
     {
         let (lits, lb) = constr.decompose();
         let mut enc = Self::from_iter(lits);
-        enc.encode_lb(lb..lb + 1, collector, var_manager);
-        collector.extend(
+        enc.encode_lb(lb..lb + 1, collector, var_manager)?;
+        collector.extend_clauses(
             enc.enforce_lb(lb)
                 .unwrap()
                 .into_iter()
                 .map(|unit| clause![unit]),
-        );
+        )?;
         Ok(())
     }
 }
@@ -154,12 +164,14 @@ pub trait BoundBoth: BoundUpper + BoundLower {
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize> + Clone,
     {
-        self.encode_ub(range.clone(), collector, var_manager);
-        self.encode_lb(range, collector, var_manager);
+        self.encode_ub(range.clone(), collector, var_manager)?;
+        self.encode_lb(range, collector, var_manager)?;
+        Ok(())
     }
     /// Returns assumptions for enforcing an equality (`sum of lits = b`) or an
     /// error if the encoding does not support one of the two required bound
@@ -174,32 +186,40 @@ pub trait BoundBoth: BoundUpper + BoundLower {
         Ok(assumps)
     }
     /// Encodes an equality cardinality constraint to CNF
+    ///
+    /// # Errors
+    ///
+    /// Either an [`Error`] of [`crate::OutOfMemory`]
     fn encode_eq_constr<Col>(
         constr: CardEQConstr,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) -> Result<(), Error>
+    ) -> anyhow::Result<()>
     where
         Col: CollectClauses,
         Self: FromIterator<Lit> + Sized,
     {
         let (lits, b) = constr.decompose();
         let mut enc = Self::from_iter(lits);
-        enc.encode_both(b..b + 1, collector, var_manager);
-        collector.extend(
+        enc.encode_both(b..b + 1, collector, var_manager)?;
+        collector.extend_clauses(
             enc.enforce_eq(b)
                 .unwrap()
                 .into_iter()
                 .map(|unit| clause![unit]),
-        );
+        )?;
         Ok(())
     }
     /// Encodes any cardinality constraint to CNF
+    ///
+    /// # Errors
+    ///
+    /// Either an [`Error`] of [`crate::OutOfMemory`]
     fn encode_constr<Col>(
         constr: CardConstraint,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) -> Result<(), Error>
+    ) -> anyhow::Result<()>
     where
         Col: CollectClauses,
         Self: FromIterator<Lit> + Sized,
@@ -235,7 +255,8 @@ pub trait BoundUpperIncremental: BoundUpper + EncodeIncremental {
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>;
 }
@@ -252,7 +273,8 @@ pub trait BoundLowerIncremental: BoundLower + EncodeIncremental {
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>;
 }
@@ -268,11 +290,12 @@ pub trait BoundBothIncremental: BoundUpperIncremental + BoundLowerIncremental {
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize> + Clone,
     {
-        self.encode_ub_change(range.clone(), collector, var_manager);
+        self.encode_ub_change(range.clone(), collector, var_manager)?;
         self.encode_lb_change(range, collector, var_manager)
     }
 }
@@ -330,7 +353,7 @@ pub fn default_encode_cardinality_constraint<Col: CollectClauses>(
     constr: CardConstraint,
     collector: &mut Col,
     var_manager: &mut dyn ManageVars,
-) {
+) -> Result<(), crate::OutOfMemory> {
     encode_cardinality_constraint::<DefBothBounding, Col>(constr, collector, var_manager)
 }
 
@@ -339,27 +362,28 @@ pub fn encode_cardinality_constraint<CE: BoundBoth + FromIterator<Lit>, Col: Col
     constr: CardConstraint,
     collector: &mut Col,
     var_manager: &mut dyn ManageVars,
-) {
+) -> Result<(), crate::OutOfMemory> {
     if constr.is_tautology() {
-        return;
+        return Ok(());
     }
     if constr.is_unsat() {
-        collector.extend([Clause::new()]);
-        return;
+        return collector.add_clause(Clause::new());
     }
     if constr.is_positive_assignment() {
-        collector.extend(constr.into_lits().into_iter().map(|lit| clause![lit]));
-        return;
+        return collector.extend_clauses(constr.into_lits().into_iter().map(|lit| clause![lit]));
     }
     if constr.is_negative_assignment() {
-        collector.extend(constr.into_lits().into_iter().map(|lit| clause![!lit]));
-        return;
+        return collector.extend_clauses(constr.into_lits().into_iter().map(|lit| clause![!lit]));
     }
     if constr.is_clause() {
-        collector.extend([constr.into_clause().unwrap()]);
-        return;
+        return collector.add_clause(constr.into_clause().unwrap());
+    }
+    match CE::encode_constr(constr, collector, var_manager) {
+        Ok(_) => Ok(()),
+        Err(err) => Err(err
+            .downcast::<crate::OutOfMemory>()
+            .expect("unexpected error when encoding constraint")),
     }
-    CE::encode_constr(constr, collector, var_manager).unwrap()
 }
 
 fn prepare_ub_range<Enc: Encode, R: RangeBounds<usize>>(enc: &Enc, range: R) -> Range<usize> {
diff --git a/rustsat/src/encodings/card/dbtotalizer.rs b/rustsat/src/encodings/card/dbtotalizer.rs
index 59f10b11..099d823f 100644
--- a/rustsat/src/encodings/card/dbtotalizer.rs
+++ b/rustsat/src/encodings/card/dbtotalizer.rs
@@ -99,7 +99,12 @@ impl EncodeIncremental for DbTotalizer {
 }
 
 impl BoundUpper for DbTotalizer {
-    fn encode_ub<Col, R>(&mut self, range: R, collector: &mut Col, var_manager: &mut dyn ManageVars)
+    fn encode_ub<Col, R>(
+        &mut self,
+        range: R,
+        collector: &mut Col,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<(), crate::OutOfMemory>
     where
         Col: CollectClauses,
         R: RangeBounds<usize>,
@@ -141,24 +146,26 @@ impl BoundUpperIncremental for DbTotalizer {
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>,
     {
         let range = super::prepare_ub_range(self, range);
         if range.is_empty() {
-            return;
+            return Ok(());
         }
         self.extend_tree();
         if let Some(id) = self.root {
             let n_vars_before = var_manager.n_used();
             let n_clauses_before = collector.n_clauses();
             for idx in range {
-                self.db.define_pos_tot(id, idx, collector, var_manager);
+                self.db.define_pos_tot(id, idx, collector, var_manager)?;
             }
             self.n_clauses += collector.n_clauses() - n_clauses_before;
             self.n_vars += var_manager.n_used() - n_vars_before;
-        }
+        };
+        Ok(())
     }
 }
 
@@ -639,7 +646,7 @@ impl TotDb {
         val: usize,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) -> Option<Lit>
+    ) -> Result<Option<Lit>, crate::OutOfMemory>
     where
         Col: CollectClauses,
     {
@@ -649,23 +656,28 @@ impl TotDb {
             Node::Leaf(lit) => {
                 debug_assert_eq!(val, 1);
                 if val != 1 {
-                    return None;
+                    return Ok(None);
                 }
-                Some(*lit)
+                Ok(Some(*lit))
             }
             Node::Unit(node) => {
                 if val > node.lits.len() || val == 0 {
-                    return None;
+                    return Ok(None);
                 }
 
                 // Check if already encoded
                 if let LitData::Lit { lit, enc_pos, .. } = node.lits[val - 1] {
                     if enc_pos {
-                        return Some(lit);
+                        return Ok(Some(lit));
                     }
                 }
 
-                Some(self.define_pos_tot(id, val - 1, collector, var_manager))
+                Ok(Some(self.define_pos_tot(
+                    id,
+                    val - 1,
+                    collector,
+                    var_manager,
+                )?))
             }
             Node::General(node) => {
                 // Check if already encoded
@@ -674,10 +686,10 @@ impl TotDb {
                         lit, enc_pos: true, ..
                     } = lit_data
                     {
-                        return Some(*lit);
+                        return Ok(Some(*lit));
                     }
                 } else {
-                    return None;
+                    return Ok(None);
                 }
 
                 debug_assert!(val <= node.max_val);
@@ -698,16 +710,16 @@ impl TotDb {
                 // Propagate value
                 if lcon.is_possible(val) && lcon.rev_map(val) <= self[lcon.id].max_val() {
                     if let Some(llit) =
-                        self.define_pos(lcon.id, lcon.rev_map(val), collector, var_manager)
+                        self.define_pos(lcon.id, lcon.rev_map(val), collector, var_manager)?
                     {
-                        collector.extend([atomics::lit_impl_lit(llit, olit)]);
+                        collector.add_clause(atomics::lit_impl_lit(llit, olit))?;
                     }
                 }
                 if rcon.is_possible(val) && rcon.rev_map(val) <= self[rcon.id].max_val() {
                     if let Some(rlit) =
-                        self.define_pos(rcon.id, rcon.rev_map(val), collector, var_manager)
+                        self.define_pos(rcon.id, rcon.rev_map(val), collector, var_manager)?
                     {
-                        collector.extend([atomics::lit_impl_lit(rlit, olit)]);
+                        collector.add_clause(atomics::lit_impl_lit(rlit, olit))?;
                     };
                 }
 
@@ -721,15 +733,16 @@ impl TotDb {
                         let rval_rev = rcon.rev_map(rval);
                         if rcon.is_possible(rval) && rval_rev <= rmax {
                             if let Some(rlit) =
-                                self.define_pos(rcon.id, rval_rev, collector, var_manager)
+                                self.define_pos(rcon.id, rval_rev, collector, var_manager)?
                             {
                                 debug_assert!(
                                     lcon.len_limit.is_none() || lcon.offset() + 1 == lval
                                 );
                                 let llit = self
-                                    .define_pos(lcon.id, lval, collector, var_manager)
+                                    .define_pos(lcon.id, lval, collector, var_manager)?
                                     .unwrap();
-                                collector.extend([atomics::cube_impl_lit(&[llit, rlit], olit)]);
+                                collector
+                                    .add_clause(atomics::cube_impl_lit(&[llit, rlit], olit))?;
                             }
                         }
                     }
@@ -741,7 +754,7 @@ impl TotDb {
                     LitData::Lit { enc_pos, .. } => *enc_pos = true,
                 };
 
-                Some(olit)
+                Ok(Some(olit))
             }
         }
     }
@@ -756,7 +769,7 @@ impl TotDb {
         idx: usize,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) -> Lit
+    ) -> Result<Lit, crate::OutOfMemory>
     where
         Col: CollectClauses,
     {
@@ -764,7 +777,7 @@ impl TotDb {
         debug_assert!(idx < node.max_val());
         if node.is_leaf() {
             debug_assert_eq!(idx, 0);
-            return node[1];
+            return Ok(node[1]);
         }
         let lcon = node.left().unwrap();
         let rcon = node.right().unwrap();
@@ -777,7 +790,7 @@ impl TotDb {
         // Check if already encoded
         if let LitData::Lit { lit, enc_pos, .. } = node.lits[idx] {
             if enc_pos {
-                return lit;
+                return Ok(lit);
             }
         }
 
@@ -803,10 +816,10 @@ impl TotDb {
 
         // Encode children (recurse)
         for lidx in l_min_idx..=l_max_idx {
-            self.define_pos_tot(lcon.id, con_idx(lidx, lcon), collector, var_manager);
+            self.define_pos_tot(lcon.id, con_idx(lidx, lcon), collector, var_manager)?;
         }
         for ridx in r_min_idx..=r_max_idx {
-            self.define_pos_tot(rcon.id, con_idx(ridx, rcon), collector, var_manager);
+            self.define_pos_tot(rcon.id, con_idx(ridx, rcon), collector, var_manager)?;
         }
 
         // Reserve variable for this node, if needed
@@ -840,16 +853,16 @@ impl TotDb {
 
         // Encode this node
         if l_max_idx == idx {
-            collector.extend([atomics::lit_impl_lit(
+            collector.add_clause(atomics::lit_impl_lit(
                 *llits[con_idx(idx, lcon)].lit().unwrap(),
                 olit,
-            )]);
+            ))?;
         }
         if r_max_idx == idx {
-            collector.extend([atomics::lit_impl_lit(
+            collector.add_clause(atomics::lit_impl_lit(
                 *rlits[con_idx(idx, rcon)].lit().unwrap(),
                 olit,
-            )]);
+            ))?;
         }
         let clause_for_lidx = |lidx: usize| {
             let ridx = idx - lidx - 1;
@@ -859,7 +872,7 @@ impl TotDb {
             atomics::cube_impl_lit(&[llit, rlit], olit)
         };
         let clause_iter = (l_min_idx..cmp::min(l_max_idx + 1, idx)).map(clause_for_lidx);
-        collector.extend(clause_iter);
+        collector.extend_clauses(clause_iter)?;
 
         // Mark positive literal as encoded
         match &mut self[id].mut_unit().lits[idx] {
@@ -867,7 +880,7 @@ impl TotDb {
             LitData::Lit { enc_pos, .. } => *enc_pos = true,
         };
 
-        olit
+        Ok(olit)
     }
 
     /// Recursively reserves all variables in the subtree rooted at the given node
@@ -1045,7 +1058,8 @@ pub mod referenced {
             range: R,
             collector: &mut Col,
             var_manager: &mut dyn ManageVars,
-        ) where
+        ) -> Result<(), crate::OutOfMemory>
+        where
             Col: CollectClauses,
             R: std::ops::RangeBounds<usize>,
         {
@@ -1081,7 +1095,8 @@ pub mod referenced {
             range: R,
             collector: &mut Col,
             var_manager: &mut dyn ManageVars,
-        ) where
+        ) -> Result<(), crate::OutOfMemory>
+        where
             Col: CollectClauses,
             R: std::ops::RangeBounds<usize>,
         {
@@ -1117,18 +1132,20 @@ pub mod referenced {
             range: R,
             collector: &mut Col,
             var_manager: &mut dyn ManageVars,
-        ) where
+        ) -> Result<(), crate::OutOfMemory>
+        where
             Col: CollectClauses,
             R: std::ops::RangeBounds<usize>,
         {
             let range = super::super::prepare_ub_range(self, range);
             if range.is_empty() {
-                return;
+                return Ok(());
             }
             for idx in range {
                 self.db
-                    .define_pos_tot(self.root, idx, collector, var_manager);
+                    .define_pos_tot(self.root, idx, collector, var_manager)?;
             }
+            Ok(())
         }
     }
 
@@ -1138,19 +1155,21 @@ pub mod referenced {
             range: R,
             collector: &mut Col,
             var_manager: &mut dyn ManageVars,
-        ) where
+        ) -> Result<(), crate::OutOfMemory>
+        where
             Col: CollectClauses,
             R: std::ops::RangeBounds<usize>,
         {
             let range = super::super::prepare_ub_range(self, range);
             if range.is_empty() {
-                return;
+                return Ok(());
             }
             for idx in range {
                 self.db
                     .borrow_mut()
-                    .define_pos_tot(self.root, idx, collector, var_manager);
+                    .define_pos_tot(self.root, idx, collector, var_manager)?;
             }
+            Ok(())
         }
     }
 }
@@ -1177,22 +1196,26 @@ mod tests {
         var_manager.increase_next_free(var![4]);
 
         let mut cnf = Cnf::new();
-        db.define_pos_tot(root, 0, &mut cnf, &mut var_manager);
+        db.define_pos_tot(root, 0, &mut cnf, &mut var_manager)
+            .unwrap();
         debug_assert_eq!(cnf.len(), 6);
 
         db.reset_encoded();
         let mut cnf = Cnf::new();
-        db.define_pos_tot(root, 1, &mut cnf, &mut var_manager);
+        db.define_pos_tot(root, 1, &mut cnf, &mut var_manager)
+            .unwrap();
         debug_assert_eq!(cnf.len(), 9);
 
         db.reset_encoded();
         let mut cnf = Cnf::new();
-        db.define_pos_tot(root, 2, &mut cnf, &mut var_manager);
+        db.define_pos_tot(root, 2, &mut cnf, &mut var_manager)
+            .unwrap();
         debug_assert_eq!(cnf.len(), 8);
 
         db.reset_encoded();
         let mut cnf = Cnf::new();
-        db.define_pos_tot(root, 3, &mut cnf, &mut var_manager);
+        db.define_pos_tot(root, 3, &mut cnf, &mut var_manager)
+            .unwrap();
         debug_assert_eq!(cnf.len(), 3);
     }
 
@@ -1209,32 +1232,32 @@ mod tests {
         var_manager.increase_next_free(var![4]);
 
         let mut cnf = Cnf::new();
-        db.define_pos(root, 1, &mut cnf, &mut var_manager);
+        db.define_pos(root, 1, &mut cnf, &mut var_manager).unwrap();
         debug_assert_eq!(cnf.len(), 0);
 
         db.reset_encoded();
         let mut cnf = Cnf::new();
-        db.define_pos(root, 4, &mut cnf, &mut var_manager);
+        db.define_pos(root, 4, &mut cnf, &mut var_manager).unwrap();
         debug_assert_eq!(cnf.len(), 3);
 
         db.reset_encoded();
         let mut cnf = Cnf::new();
-        db.define_pos(root, 7, &mut cnf, &mut var_manager);
+        db.define_pos(root, 7, &mut cnf, &mut var_manager).unwrap();
         debug_assert_eq!(cnf.len(), 3);
 
         db.reset_encoded();
         let mut cnf = Cnf::new();
-        db.define_pos(root, 8, &mut cnf, &mut var_manager);
+        db.define_pos(root, 8, &mut cnf, &mut var_manager).unwrap();
         debug_assert_eq!(cnf.len(), 2);
 
         db.reset_encoded();
         let mut cnf = Cnf::new();
-        db.define_pos(root, 15, &mut cnf, &mut var_manager);
+        db.define_pos(root, 15, &mut cnf, &mut var_manager).unwrap();
         debug_assert_eq!(cnf.len(), 4);
 
         db.reset_encoded();
         let mut cnf = Cnf::new();
-        db.define_pos(root, 22, &mut cnf, &mut var_manager);
+        db.define_pos(root, 22, &mut cnf, &mut var_manager).unwrap();
         debug_assert_eq!(cnf.len(), 3);
     }
 
@@ -1251,32 +1274,32 @@ mod tests {
         var_manager.increase_next_free(var![3]);
 
         let mut cnf = Cnf::new();
-        db.define_pos(root, 1, &mut cnf, &mut var_manager);
+        db.define_pos(root, 1, &mut cnf, &mut var_manager).unwrap();
         debug_assert_eq!(cnf.len(), 2);
 
         db.reset_encoded();
         let mut cnf = Cnf::new();
-        db.define_pos(root, 2, &mut cnf, &mut var_manager);
+        db.define_pos(root, 2, &mut cnf, &mut var_manager).unwrap();
         debug_assert_eq!(cnf.len(), 2);
 
         db.reset_encoded();
         let mut cnf = Cnf::new();
-        db.define_pos(root, 3, &mut cnf, &mut var_manager);
+        db.define_pos(root, 3, &mut cnf, &mut var_manager).unwrap();
         debug_assert_eq!(cnf.len(), 3);
 
         db.reset_encoded();
         let mut cnf = Cnf::new();
-        db.define_pos(root, 4, &mut cnf, &mut var_manager);
+        db.define_pos(root, 4, &mut cnf, &mut var_manager).unwrap();
         debug_assert_eq!(cnf.len(), 2);
 
         db.reset_encoded();
         let mut cnf = Cnf::new();
-        db.define_pos(root, 5, &mut cnf, &mut var_manager);
+        db.define_pos(root, 5, &mut cnf, &mut var_manager).unwrap();
         debug_assert_eq!(cnf.len(), 2);
 
         db.reset_encoded();
         let mut cnf = Cnf::new();
-        db.define_pos(root, 6, &mut cnf, &mut var_manager);
+        db.define_pos(root, 6, &mut cnf, &mut var_manager).unwrap();
         debug_assert_eq!(cnf.len(), 2);
     }
 
@@ -1288,7 +1311,7 @@ mod tests {
         let mut var_manager = BasicVarManager::default();
         var_manager.increase_next_free(var![4]);
         let mut cnf = Cnf::new();
-        tot.encode_ub(0..5, &mut cnf, &mut var_manager);
+        tot.encode_ub(0..5, &mut cnf, &mut var_manager).unwrap();
         assert_eq!(tot.depth(), 3);
         println!("len: {}, {:?}", cnf.len(), cnf);
         assert_eq!(cnf.len(), 14);
@@ -1304,7 +1327,7 @@ mod tests {
         let mut var_manager = BasicVarManager::default();
         var_manager.increase_next_free(var![4]);
         let mut cnf = Cnf::new();
-        tot.encode_ub(3..4, &mut cnf, &mut var_manager);
+        tot.encode_ub(3..4, &mut cnf, &mut var_manager).unwrap();
         assert_eq!(tot.depth(), 3);
         assert_eq!(cnf.len(), 3);
         assert_eq!(cnf.len(), tot.n_clauses());
@@ -1317,14 +1340,15 @@ mod tests {
         let mut var_manager = BasicVarManager::default();
         var_manager.increase_next_free(var![4]);
         let mut cnf1 = Cnf::new();
-        tot1.encode_ub(0..5, &mut cnf1, &mut var_manager);
+        tot1.encode_ub(0..5, &mut cnf1, &mut var_manager).unwrap();
         let mut tot2 = DbTotalizer::default();
         tot2.extend(vec![lit![0], lit![1], lit![2], lit![3]]);
         let mut var_manager = BasicVarManager::default();
         var_manager.increase_next_free(var![4]);
         let mut cnf2 = Cnf::new();
-        tot2.encode_ub(0..3, &mut cnf2, &mut var_manager);
-        tot2.encode_ub_change(0..5, &mut cnf2, &mut var_manager);
+        tot2.encode_ub(0..3, &mut cnf2, &mut var_manager).unwrap();
+        tot2.encode_ub_change(0..5, &mut cnf2, &mut var_manager)
+            .unwrap();
         assert_eq!(cnf1.len(), cnf2.len());
         assert_eq!(cnf1.len(), tot1.n_clauses());
         assert_eq!(cnf2.len(), tot2.n_clauses());
diff --git a/rustsat/src/encodings/card/simulators.rs b/rustsat/src/encodings/card/simulators.rs
index ca8a1634..7f4b8ed5 100644
--- a/rustsat/src/encodings/card/simulators.rs
+++ b/rustsat/src/encodings/card/simulators.rs
@@ -121,7 +121,12 @@ impl<CE> BoundUpper for Inverted<CE>
 where
     CE: BoundLower,
 {
-    fn encode_ub<Col, R>(&mut self, range: R, collector: &mut Col, var_manager: &mut dyn ManageVars)
+    fn encode_ub<Col, R>(
+        &mut self,
+        range: R,
+        collector: &mut Col,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<(), crate::OutOfMemory>
     where
         Col: CollectClauses,
         R: RangeBounds<usize>,
@@ -147,7 +152,12 @@ impl<CE> BoundLower for Inverted<CE>
 where
     CE: BoundUpper,
 {
-    fn encode_lb<Col, R>(&mut self, range: R, collector: &mut Col, var_manager: &mut dyn ManageVars)
+    fn encode_lb<Col, R>(
+        &mut self,
+        range: R,
+        collector: &mut Col,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<(), crate::OutOfMemory>
     where
         Col: CollectClauses,
         R: RangeBounds<usize>,
@@ -178,7 +188,8 @@ where
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>,
     {
@@ -199,7 +210,8 @@ where
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>,
     {
@@ -325,7 +337,12 @@ where
     UBE: BoundUpper,
     LBE: BoundLower,
 {
-    fn encode_ub<Col, R>(&mut self, range: R, collector: &mut Col, var_manager: &mut dyn ManageVars)
+    fn encode_ub<Col, R>(
+        &mut self,
+        range: R,
+        collector: &mut Col,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<(), crate::OutOfMemory>
     where
         Col: CollectClauses,
         R: RangeBounds<usize>,
@@ -343,7 +360,12 @@ where
     UBE: BoundUpper,
     LBE: BoundLower,
 {
-    fn encode_lb<Col, R>(&mut self, range: R, collector: &mut Col, var_manager: &mut dyn ManageVars)
+    fn encode_lb<Col, R>(
+        &mut self,
+        range: R,
+        collector: &mut Col,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<(), crate::OutOfMemory>
     where
         Col: CollectClauses,
         R: RangeBounds<usize>,
@@ -366,7 +388,8 @@ where
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>,
     {
@@ -384,7 +407,8 @@ where
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>,
     {
diff --git a/rustsat/src/encodings/card/totalizer.rs b/rustsat/src/encodings/card/totalizer.rs
index 4f6e6bf2..71c65241 100644
--- a/rustsat/src/encodings/card/totalizer.rs
+++ b/rustsat/src/encodings/card/totalizer.rs
@@ -121,14 +121,19 @@ impl EncodeIncremental for Totalizer {
 }
 
 impl BoundUpper for Totalizer {
-    fn encode_ub<Col, R>(&mut self, range: R, collector: &mut Col, var_manager: &mut dyn ManageVars)
+    fn encode_ub<Col, R>(
+        &mut self,
+        range: R,
+        collector: &mut Col,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<(), crate::OutOfMemory>
     where
         Col: CollectClauses,
         R: RangeBounds<usize>,
     {
         let range = super::prepare_ub_range(self, range);
         if range.is_empty() {
-            return;
+            return Ok(());
         };
         self.extend_tree();
         match &mut self.root {
@@ -136,11 +141,12 @@ impl BoundUpper for Totalizer {
             Some(root) => {
                 let n_vars_before = var_manager.n_used();
                 let n_clauses_before = collector.n_clauses();
-                root.rec_encode_ub(range, collector, var_manager);
+                root.rec_encode_ub(range, collector, var_manager)?;
                 self.n_clauses += collector.n_clauses() - n_clauses_before;
                 self.n_vars += var_manager.n_used() - n_vars_before;
             }
-        }
+        };
+        Ok(())
     }
 
     fn enforce_ub(&self, ub: usize) -> Result<Vec<Lit>, Error> {
@@ -169,14 +175,19 @@ impl BoundUpper for Totalizer {
 }
 
 impl BoundLower for Totalizer {
-    fn encode_lb<Col, R>(&mut self, range: R, collector: &mut Col, var_manager: &mut dyn ManageVars)
+    fn encode_lb<Col, R>(
+        &mut self,
+        range: R,
+        collector: &mut Col,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<(), crate::OutOfMemory>
     where
         Col: CollectClauses,
         R: RangeBounds<usize>,
     {
         let range = super::prepare_lb_range(self, range);
         if range.is_empty() {
-            return;
+            return Ok(());
         };
         self.extend_tree();
         match &mut self.root {
@@ -184,11 +195,12 @@ impl BoundLower for Totalizer {
             Some(root) => {
                 let n_vars_before = var_manager.n_used();
                 let n_clauses_before = collector.n_clauses();
-                root.rec_encode_lb(range, collector, var_manager);
+                root.rec_encode_lb(range, collector, var_manager)?;
                 self.n_clauses += collector.n_clauses() - n_clauses_before;
                 self.n_vars += var_manager.n_used() - n_vars_before;
             }
-        }
+        };
+        Ok(())
     }
 
     fn enforce_lb(&self, lb: usize) -> Result<Vec<Lit>, Error> {
@@ -224,13 +236,14 @@ impl BoundUpperIncremental for Totalizer {
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>,
     {
         let range = super::prepare_ub_range(self, range);
         if range.is_empty() {
-            return;
+            return Ok(());
         };
         self.extend_tree();
         match &mut self.root {
@@ -238,11 +251,12 @@ impl BoundUpperIncremental for Totalizer {
             Some(root) => {
                 let n_vars_before = var_manager.n_used();
                 let n_clauses_before = collector.n_clauses();
-                root.rec_encode_ub_change(range, collector, var_manager);
+                root.rec_encode_ub_change(range, collector, var_manager)?;
                 self.n_clauses += collector.n_clauses() - n_clauses_before;
                 self.n_vars += var_manager.n_used() - n_vars_before;
             }
-        }
+        };
+        Ok(())
     }
 }
 
@@ -252,13 +266,14 @@ impl BoundLowerIncremental for Totalizer {
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>,
     {
         let range = super::prepare_lb_range(self, range);
         if range.is_empty() {
-            return;
+            return Ok(());
         };
         self.extend_tree();
         match &mut self.root {
@@ -266,11 +281,12 @@ impl BoundLowerIncremental for Totalizer {
             Some(root) => {
                 let n_vars_before = var_manager.n_used();
                 let n_clauses_before = collector.n_clauses();
-                root.rec_encode_lb_change(range, collector, var_manager);
+                root.rec_encode_lb_change(range, collector, var_manager)?;
                 self.n_clauses += collector.n_clauses() - n_clauses_before;
                 self.n_vars += var_manager.n_used() - n_vars_before;
             }
-        }
+        };
+        Ok(())
     }
 }
 
@@ -391,12 +407,13 @@ impl Node {
         range: Range<usize>,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
     {
         let range = self.limit_range(range);
         if range.is_empty() {
-            return;
+            return Ok(());
         }
 
         // Reserve vars if needed
@@ -449,9 +466,11 @@ impl Node {
                     (0..=right_lits.len())
                         .filter_map(move |right_val| clause_for_vals(left_val, right_val))
                 });
-                collector.extend(clause_iter);
+                collector.extend_clauses(clause_iter)?;
             }
-        }
+        };
+
+        Ok(())
     }
 
     /// Encodes the lower bound adder for this node in a given range. This
@@ -462,12 +481,13 @@ impl Node {
         range: Range<usize>,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
     {
         let range = self.limit_range(range);
         if range.is_empty() {
-            return;
+            return Ok(());
         }
 
         // Reserve vars if needed
@@ -527,9 +547,11 @@ impl Node {
                     (0..=right_lits.len())
                         .filter_map(move |right_val| clause_for_vals(left_val, right_val))
                 });
-                collector.extend(clause_iter);
+                collector.extend_clauses(clause_iter)?;
             }
-        }
+        };
+
+        Ok(())
     }
 
     /// Encodes the upper bound adder from the children to this node in a given
@@ -540,12 +562,13 @@ impl Node {
         range: Range<usize>,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
     {
         let range = self.limit_range(range);
         if range.is_empty() {
-            return;
+            return Ok(());
         }
 
         match self {
@@ -562,16 +585,17 @@ impl Node {
                 let left_range = Node::compute_required_range(range.clone(), right.max_val());
                 let right_range = Node::compute_required_range(range.clone(), left.max_val());
                 // Recurse
-                left.rec_encode_ub(left_range, collector, var_manager);
-                right.rec_encode_ub(right_range, collector, var_manager);
+                left.rec_encode_ub(left_range, collector, var_manager)?;
+                right.rec_encode_ub(right_range, collector, var_manager)?;
 
                 // Ignore all previous encoding and encode from scratch
                 let n_clauses_before = collector.n_clauses();
-                self.encode_ub_range(range.clone(), collector, var_manager);
+                self.encode_ub_range(range.clone(), collector, var_manager)?;
 
                 self.update_stats(range, lb_range, collector.n_clauses() - n_clauses_before);
             }
         }
+        Ok(())
     }
 
     /// Encodes the lower bound adder from the children to this node in a given
@@ -582,12 +606,13 @@ impl Node {
         range: Range<usize>,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
     {
         let range = self.limit_range(range);
         if range.is_empty() {
-            return;
+            return Ok(());
         }
 
         match self {
@@ -604,16 +629,18 @@ impl Node {
                 let left_range = Node::compute_required_range(range.clone(), right.max_val());
                 let right_range = Node::compute_required_range(range.clone(), left.max_val());
                 // Recurse
-                left.rec_encode_lb(left_range, collector, var_manager);
-                right.rec_encode_lb(right_range, collector, var_manager);
+                left.rec_encode_lb(left_range, collector, var_manager)?;
+                right.rec_encode_lb(right_range, collector, var_manager)?;
 
                 // Ignore all previous encoding and encode from scratch
                 let n_clauses_before = collector.n_clauses();
-                self.encode_lb_range(range.clone(), collector, var_manager);
+                self.encode_lb_range(range.clone(), collector, var_manager)?;
 
                 self.update_stats(ub_range, range, collector.n_clauses() - n_clauses_before);
             }
-        }
+        };
+
+        Ok(())
     }
 
     /// Encodes the upper bound adder from the children to this node in a given
@@ -623,12 +650,13 @@ impl Node {
         range: Range<usize>,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
     {
         let range = self.limit_range(range);
         if range.is_empty() {
-            return;
+            return Ok(());
         }
 
         match self {
@@ -647,27 +675,29 @@ impl Node {
                 let left_range = Node::compute_required_range(range.clone(), right.max_val());
                 let right_range = Node::compute_required_range(range.clone(), left.max_val());
                 // Recurse
-                left.rec_encode_ub_change(left_range, collector, var_manager);
-                right.rec_encode_ub_change(right_range, collector, var_manager);
+                left.rec_encode_ub_change(left_range, collector, var_manager)?;
+                right.rec_encode_ub_change(right_range, collector, var_manager)?;
 
                 // Encode changes for current node
                 let n_clauses_before = collector.n_clauses();
                 if ub_range.is_empty() {
                     // First time encoding this node
-                    self.encode_ub_range(range.clone(), collector, var_manager)
+                    self.encode_ub_range(range.clone(), collector, var_manager)?;
                 } else {
                     // Part already encoded
                     if range.start < ub_range.start {
-                        self.encode_ub_range(range.start..ub_range.start, collector, var_manager);
+                        self.encode_ub_range(range.start..ub_range.start, collector, var_manager)?;
                     };
                     if range.end > ub_range.end {
-                        self.encode_ub_range(ub_range.end..range.end, collector, var_manager);
+                        self.encode_ub_range(ub_range.end..range.end, collector, var_manager)?;
                     };
                 };
 
                 self.update_stats(range, lb_range, collector.n_clauses() - n_clauses_before);
             }
-        }
+        };
+
+        Ok(())
     }
 
     /// Encodes the lower bound adder from the children to this node in a given
@@ -677,7 +707,8 @@ impl Node {
         range: Range<usize>,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
     {
         match self {
@@ -696,27 +727,29 @@ impl Node {
                 let left_range = Node::compute_required_range(range.clone(), right.max_val());
                 let right_range = Node::compute_required_range(range.clone(), left.max_val());
                 // Recurse
-                left.rec_encode_lb_change(left_range, collector, var_manager);
-                right.rec_encode_lb_change(right_range, collector, var_manager);
+                left.rec_encode_lb_change(left_range, collector, var_manager)?;
+                right.rec_encode_lb_change(right_range, collector, var_manager)?;
 
                 // Encode changes for current node
                 let n_clauses_before = collector.n_clauses();
                 if lb_range.is_empty() {
                     // First time encoding this node
-                    self.encode_lb_range(range.clone(), collector, var_manager)
+                    self.encode_lb_range(range.clone(), collector, var_manager)?;
                 } else {
                     // Part already encoded
                     if range.start < lb_range.start {
-                        self.encode_lb_range(range.start..lb_range.start, collector, var_manager);
+                        self.encode_lb_range(range.start..lb_range.start, collector, var_manager)?;
                     };
                     if range.end > lb_range.end {
-                        self.encode_lb_range(lb_range.end..range.end, collector, var_manager);
+                        self.encode_lb_range(lb_range.end..range.end, collector, var_manager)?;
                     };
                 };
 
                 self.update_stats(ub_range, range, collector.n_clauses() - n_clauses_before);
             }
-        }
+        };
+
+        Ok(())
     }
 
     /// Reserves variables this node might need for indices in a given range.
@@ -854,8 +887,10 @@ mod tests {
         let mut var_manager = BasicVarManager::default();
         var_manager.increase_next_free(var![2]);
         let mut cnf = Cnf::new();
-        node.encode_ub_range(0..3, &mut cnf, &mut var_manager);
-        node.encode_lb_range(0..3, &mut cnf, &mut var_manager);
+        node.encode_ub_range(0..3, &mut cnf, &mut var_manager)
+            .unwrap();
+        node.encode_lb_range(0..3, &mut cnf, &mut var_manager)
+            .unwrap();
         match &node {
             Node::Leaf { .. } => panic!(),
             Node::Internal { out_lits, .. } => assert_eq!(out_lits.len(), 2),
@@ -892,8 +927,10 @@ mod tests {
         let mut var_manager = BasicVarManager::default();
         var_manager.increase_next_free(var![5]);
         let mut cnf = Cnf::new();
-        node.encode_ub_range(0..5, &mut cnf, &mut var_manager);
-        node.encode_lb_range(0..5, &mut cnf, &mut var_manager);
+        node.encode_ub_range(0..5, &mut cnf, &mut var_manager)
+            .unwrap();
+        node.encode_lb_range(0..5, &mut cnf, &mut var_manager)
+            .unwrap();
         match &node {
             Node::Leaf { .. } => panic!(),
             Node::Internal { out_lits, .. } => assert_eq!(out_lits.len(), 4),
@@ -910,7 +947,8 @@ mod tests {
         let mut var_manager = BasicVarManager::default();
         var_manager.increase_next_free(var![2]);
         let mut cnf = Cnf::new();
-        node.encode_lb_range(0..2, &mut cnf, &mut var_manager);
+        node.encode_lb_range(0..2, &mut cnf, &mut var_manager)
+            .unwrap();
         match &node {
             Node::Leaf { .. } => panic!(),
             Node::Internal { out_lits, .. } => assert_eq!(out_lits.len(), 1),
@@ -947,8 +985,10 @@ mod tests {
         let mut var_manager = BasicVarManager::default();
         var_manager.increase_next_free(var![7]);
         let mut cnf = Cnf::new();
-        node.encode_ub_range(0..4, &mut cnf, &mut var_manager);
-        node.encode_lb_range(0..4, &mut cnf, &mut var_manager);
+        node.encode_ub_range(0..4, &mut cnf, &mut var_manager)
+            .unwrap();
+        node.encode_lb_range(0..4, &mut cnf, &mut var_manager)
+            .unwrap();
         match &node {
             Node::Leaf { .. } => panic!(),
             Node::Internal { out_lits, .. } => assert_eq!(out_lits.len(), 4),
@@ -985,8 +1025,10 @@ mod tests {
         let mut var_manager = BasicVarManager::default();
         var_manager.increase_next_free(var![7]);
         let mut cnf = Cnf::new();
-        node.encode_ub_range(3..3, &mut cnf, &mut var_manager);
-        node.encode_lb_range(3..3, &mut cnf, &mut var_manager);
+        node.encode_ub_range(3..3, &mut cnf, &mut var_manager)
+            .unwrap();
+        node.encode_lb_range(3..3, &mut cnf, &mut var_manager)
+            .unwrap();
         assert_eq!(cnf.len(), 0);
     }
 
@@ -1019,8 +1061,10 @@ mod tests {
         let mut var_manager = BasicVarManager::default();
         var_manager.increase_next_free(var![7]);
         let mut cnf = Cnf::new();
-        node.encode_ub_range(2..4, &mut cnf, &mut var_manager);
-        node.encode_lb_range(2..4, &mut cnf, &mut var_manager);
+        node.encode_ub_range(2..4, &mut cnf, &mut var_manager)
+            .unwrap();
+        node.encode_lb_range(2..4, &mut cnf, &mut var_manager)
+            .unwrap();
         match &node {
             Node::Leaf { .. } => panic!(),
             Node::Internal { out_lits, .. } => assert_eq!(out_lits.len(), 4),
@@ -1037,8 +1081,8 @@ mod tests {
         let mut var_manager = BasicVarManager::default();
         var_manager.increase_next_free(var![4]);
         let mut cnf = Cnf::new();
-        tot.encode_ub(0..5, &mut cnf, &mut var_manager);
-        tot.encode_lb(0..5, &mut cnf, &mut var_manager);
+        tot.encode_ub(0..5, &mut cnf, &mut var_manager).unwrap();
+        tot.encode_lb(0..5, &mut cnf, &mut var_manager).unwrap();
         assert_eq!(tot.depth(), 3);
         assert_eq!(cnf.len(), 28);
         assert_eq!(tot.n_clauses(), 28);
@@ -1054,7 +1098,7 @@ mod tests {
         let mut var_manager = BasicVarManager::default();
         var_manager.increase_next_free(var![4]);
         let mut cnf = Cnf::new();
-        tot.encode_both(3..4, &mut cnf, &mut var_manager);
+        tot.encode_both(3..4, &mut cnf, &mut var_manager).unwrap();
         assert_eq!(tot.depth(), 3);
         assert_eq!(cnf.len(), 12);
         assert_eq!(cnf.len(), tot.n_clauses());
@@ -1067,14 +1111,15 @@ mod tests {
         let mut var_manager = BasicVarManager::default();
         var_manager.increase_next_free(var![4]);
         let mut cnf1 = Cnf::new();
-        tot1.encode_ub(0..5, &mut cnf1, &mut var_manager);
+        tot1.encode_ub(0..5, &mut cnf1, &mut var_manager).unwrap();
         let mut tot2 = Totalizer::default();
         tot2.extend(vec![lit![0], lit![1], lit![2], lit![3]]);
         let mut var_manager = BasicVarManager::default();
         var_manager.increase_next_free(var![4]);
         let mut cnf2 = Cnf::new();
-        tot2.encode_ub(0..3, &mut cnf2, &mut var_manager);
-        tot2.encode_ub_change(0..5, &mut cnf2, &mut var_manager);
+        tot2.encode_ub(0..3, &mut cnf2, &mut var_manager).unwrap();
+        tot2.encode_ub_change(0..5, &mut cnf2, &mut var_manager)
+            .unwrap();
         assert_eq!(cnf1.len(), cnf2.len());
         assert_eq!(cnf1.len(), tot1.n_clauses());
         assert_eq!(cnf2.len(), tot2.n_clauses());
@@ -1087,14 +1132,15 @@ mod tests {
         let mut var_manager = BasicVarManager::default();
         var_manager.increase_next_free(var![4]);
         let mut cnf1 = Cnf::new();
-        tot1.encode_lb(0..5, &mut cnf1, &mut var_manager);
+        tot1.encode_lb(0..5, &mut cnf1, &mut var_manager).unwrap();
         let mut tot2 = Totalizer::default();
         tot2.extend(vec![lit![0], lit![1], lit![2], lit![3]]);
         let mut var_manager = BasicVarManager::default();
         var_manager.increase_next_free(var![4]);
         let mut cnf2 = Cnf::new();
-        tot2.encode_lb(0..3, &mut cnf2, &mut var_manager);
-        tot2.encode_lb_change(0..5, &mut cnf2, &mut var_manager);
+        tot2.encode_lb(0..3, &mut cnf2, &mut var_manager).unwrap();
+        tot2.encode_lb_change(0..5, &mut cnf2, &mut var_manager)
+            .unwrap();
         assert_eq!(cnf1.len(), cnf2.len());
         assert_eq!(cnf1.len(), tot1.n_clauses());
         assert_eq!(cnf2.len(), tot2.n_clauses());
diff --git a/rustsat/src/encodings/pb.rs b/rustsat/src/encodings/pb.rs
index bb426bf9..b8f1e470 100644
--- a/rustsat/src/encodings/pb.rs
+++ b/rustsat/src/encodings/pb.rs
@@ -91,7 +91,8 @@ pub trait BoundUpper: Encode {
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>;
     /// Returns assumptions/units for enforcing an upper bound (`weighted sum of
@@ -100,29 +101,33 @@ pub trait BoundUpper: Encode {
     /// [`Error::NotEncoded`] will be returned.
     fn enforce_ub(&self, ub: usize) -> Result<Vec<Lit>, Error>;
     /// Encodes an upper bound pseudo-boolean constraint to CNF
+    ///
+    /// # Errors
+    ///
+    /// Either an [`Error`] of [`crate::OutOfMemory`]
     fn encode_ub_constr<Col>(
         constr: PBUBConstr,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) -> Result<(), Error>
+    ) -> anyhow::Result<()>
     where
         Col: CollectClauses,
         Self: FromIterator<(Lit, usize)> + Sized,
     {
         let (lits, ub) = constr.decompose();
         let ub = if ub < 0 {
-            return Err(Error::Unsat);
+            anyhow::bail!(Error::Unsat);
         } else {
             ub as usize
         };
         let mut enc = Self::from_iter(lits);
-        enc.encode_ub(ub..ub + 1, collector, var_manager);
-        collector.extend(
+        enc.encode_ub(ub..ub + 1, collector, var_manager)?;
+        collector.extend_clauses(
             enc.enforce_ub(ub)
                 .unwrap()
                 .into_iter()
                 .map(|unit| clause![unit]),
-        );
+        )?;
         Ok(())
     }
     /// Gets the next smaller upper bound value that can be _easily_ encoded. This
@@ -145,7 +150,8 @@ pub trait BoundLower: Encode {
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>;
     /// Returns assumptions/units for enforcing a lower bound (`sum of lits >=
@@ -156,11 +162,15 @@ pub trait BoundLower: Encode {
     /// is returned.
     fn enforce_lb(&self, lb: usize) -> Result<Vec<Lit>, Error>;
     /// Encodes a lower bound pseudo-boolean constraint to CNF
+    ///
+    /// # Errors
+    ///
+    /// Either an [`Error`] of [`crate::OutOfMemory`]
     fn encode_lb_constr<Col>(
         constr: PBLBConstr,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) -> Result<(), Error>
+    ) -> anyhow::Result<()>
     where
         Col: CollectClauses,
         Self: FromIterator<(Lit, usize)> + Sized,
@@ -172,13 +182,13 @@ pub trait BoundLower: Encode {
             lb as usize
         };
         let mut enc = Self::from_iter(lits);
-        enc.encode_lb(lb..lb + 1, collector, var_manager);
-        collector.extend(
+        enc.encode_lb(lb..lb + 1, collector, var_manager)?;
+        collector.extend_clauses(
             enc.enforce_lb(lb)
                 .unwrap()
                 .into_iter()
                 .map(|unit| clause![unit]),
-        );
+        )?;
         Ok(())
     }
     /// Gets the next greater lower bound value that can be _easily_ encoded. This
@@ -199,12 +209,14 @@ pub trait BoundBoth: BoundUpper + BoundLower {
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize> + Clone,
     {
-        self.encode_ub(range.clone(), collector, var_manager);
-        self.encode_lb(range, collector, var_manager);
+        self.encode_ub(range.clone(), collector, var_manager)?;
+        self.encode_lb(range, collector, var_manager)?;
+        Ok(())
     }
     /// Returns assumptions for enforcing an equality (`sum of lits = b`) or an
     /// error if the encoding does not support one of the two required bound
@@ -219,37 +231,45 @@ pub trait BoundBoth: BoundUpper + BoundLower {
         Ok(assumps)
     }
     /// Encodes an equality pseudo-boolean constraint to CNF
+    ///
+    /// # Errors
+    ///
+    /// Either an [`Error`] of [`crate::OutOfMemory`]
     fn encode_eq_constr<Col>(
         constr: PBEQConstr,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) -> Result<(), Error>
+    ) -> anyhow::Result<()>
     where
         Col: CollectClauses,
         Self: FromIterator<(Lit, usize)> + Sized,
     {
         let (lits, b) = constr.decompose();
         let b = if b < 0 {
-            return Err(Error::Unsat);
+            anyhow::bail!(Error::Unsat);
         } else {
             b as usize
         };
         let mut enc = Self::from_iter(lits);
-        enc.encode_both(b..b + 1, collector, var_manager);
-        collector.extend(
+        enc.encode_both(b..b + 1, collector, var_manager)?;
+        collector.extend_clauses(
             enc.enforce_eq(b)
                 .unwrap()
                 .into_iter()
                 .map(|unit| clause![unit]),
-        );
+        )?;
         Ok(())
     }
     /// Encodes any pseudo-boolean constraint to CNF
+    ///
+    /// # Errors
+    ///
+    /// Either an [`Error`] of [`crate::OutOfMemory`]
     fn encode_constr<Col>(
         constr: PBConstraint,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) -> Result<(), Error>
+    ) -> anyhow::Result<()>
     where
         Col: CollectClauses,
         Self: FromIterator<(Lit, usize)> + Sized,
@@ -285,7 +305,8 @@ pub trait BoundUpperIncremental: BoundUpper + EncodeIncremental {
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>;
 }
@@ -302,7 +323,8 @@ pub trait BoundLowerIncremental: BoundLower + EncodeIncremental {
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>;
 }
@@ -318,12 +340,14 @@ pub trait BoundBothIncremental: BoundUpperIncremental + BoundLowerIncremental {
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize> + Clone,
     {
-        self.encode_ub_change(range.clone(), collector, var_manager);
-        self.encode_lb_change(range, collector, var_manager);
+        self.encode_ub_change(range.clone(), collector, var_manager)?;
+        self.encode_lb_change(range, collector, var_manager)?;
+        Ok(())
     }
 }
 
@@ -381,7 +405,7 @@ pub fn default_encode_pb_constraint<Col: CollectClauses>(
     constr: PBConstraint,
     collector: &mut Col,
     var_manager: &mut dyn ManageVars,
-) {
+) -> Result<(), crate::OutOfMemory> {
     encode_pb_constraint::<DefBothBounding, Col>(constr, collector, var_manager)
 }
 
@@ -390,31 +414,34 @@ pub fn encode_pb_constraint<PBE: BoundBoth + FromIterator<(Lit, usize)>, Col: Co
     constr: PBConstraint,
     collector: &mut Col,
     var_manager: &mut dyn ManageVars,
-) {
+) -> Result<(), crate::OutOfMemory> {
     if constr.is_tautology() {
-        return;
+        return Ok(());
     }
     if constr.is_unsat() {
-        collector.extend([Clause::new()]);
-        return;
+        return collector.add_clause(Clause::new());
     }
     if constr.is_positive_assignment() {
-        collector.extend(constr.into_lits().into_iter().map(|(lit, _)| clause![lit]));
-        return;
+        return collector
+            .extend_clauses(constr.into_lits().into_iter().map(|(lit, _)| clause![lit]));
     }
     if constr.is_negative_assignment() {
-        collector.extend(constr.into_lits().into_iter().map(|(lit, _)| clause![!lit]));
-        return;
+        return collector
+            .extend_clauses(constr.into_lits().into_iter().map(|(lit, _)| clause![!lit]));
     }
     if constr.is_clause() {
-        collector.extend([constr.into_clause().unwrap()]);
-        return;
+        return collector.add_clause(constr.into_clause().unwrap());
     }
     if constr.is_card() {
         let card = constr.into_card_constr().unwrap();
         return card::default_encode_cardinality_constraint(card, collector, var_manager);
     }
-    PBE::encode_constr(constr, collector, var_manager).unwrap()
+    match PBE::encode_constr(constr, collector, var_manager) {
+        Ok(_) => Ok(()),
+        Err(err) => Err(err
+            .downcast::<crate::OutOfMemory>()
+            .expect("unexpected error when encoding constraint")),
+    }
 }
 
 fn prepare_ub_range<Enc: Encode, R: RangeBounds<usize>>(enc: &Enc, range: R) -> Range<usize> {
diff --git a/rustsat/src/encodings/pb/dbgte.rs b/rustsat/src/encodings/pb/dbgte.rs
index 04552b65..8187c048 100644
--- a/rustsat/src/encodings/pb/dbgte.rs
+++ b/rustsat/src/encodings/pb/dbgte.rs
@@ -158,13 +158,18 @@ impl EncodeIncremental for DbGte {
 }
 
 impl BoundUpper for DbGte {
-    fn encode_ub<Col, R>(&mut self, range: R, collector: &mut Col, var_manager: &mut dyn ManageVars)
+    fn encode_ub<Col, R>(
+        &mut self,
+        range: R,
+        collector: &mut Col,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<(), crate::OutOfMemory>
     where
         Col: CollectClauses,
         R: RangeBounds<usize>,
     {
         self.db.reset_encoded();
-        self.encode_ub_change(range, collector, var_manager);
+        self.encode_ub_change(range, collector, var_manager)
     }
 
     fn enforce_ub(&self, ub: usize) -> Result<Vec<Lit>, Error> {
@@ -221,13 +226,14 @@ impl BoundUpperIncremental for DbGte {
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>,
     {
         let range = super::prepare_ub_range(self, range);
         if range.is_empty() {
-            return;
+            return Ok(());
         }
         let n_vars_before = var_manager.n_used();
         let n_clauses_before = collector.n_clauses();
@@ -238,14 +244,16 @@ impl BoundUpperIncremental for DbGte {
                     con.rev_map_round_up(range.start + 1)
                         ..=con.rev_map(range.end + self.max_leaf_weight),
                 )
-                .for_each(|val| {
+                .try_for_each(|val| {
                     self.db
-                        .define_pos(con.id, val, collector, var_manager)
+                        .define_pos(con.id, val, collector, var_manager)?
                         .unwrap();
-                })
+                    Ok::<(), crate::OutOfMemory>(())
+                })?
         }
         self.n_clauses += collector.n_clauses() - n_clauses_before;
         self.n_vars += var_manager.n_used() - n_vars_before;
+        Ok(())
     }
 }
 
@@ -435,7 +443,8 @@ pub mod referenced {
             range: R,
             collector: &mut Col,
             var_manager: &mut dyn ManageVars,
-        ) where
+        ) -> Result<(), crate::OutOfMemory>
+        where
             Col: CollectClauses,
             R: RangeBounds<usize>,
         {
@@ -490,7 +499,8 @@ pub mod referenced {
             range: R,
             collector: &mut Col,
             var_manager: &mut dyn ManageVars,
-        ) where
+        ) -> Result<(), crate::OutOfMemory>
+        where
             Col: CollectClauses,
             R: RangeBounds<usize>,
         {
@@ -545,24 +555,27 @@ pub mod referenced {
             range: R,
             collector: &mut Col,
             var_manager: &mut dyn ManageVars,
-        ) where
+        ) -> Result<(), crate::OutOfMemory>
+        where
             Col: CollectClauses,
             R: RangeBounds<usize>,
         {
             let range = super::super::prepare_ub_range(self, range);
             if range.is_empty() {
-                return;
+                return Ok(());
             }
             self.db[self.root.id]
                 .vals(
                     self.root.rev_map_round_up(range.start + 1)
                         ..=self.root.rev_map(range.end + self.max_leaf_weight),
                 )
-                .for_each(|val| {
+                .try_for_each(|val| {
                     self.db
-                        .define_pos(self.root.id, val, collector, var_manager)
+                        .define_pos(self.root.id, val, collector, var_manager)?
                         .unwrap();
-                });
+                    Ok::<(), crate::OutOfMemory>(())
+                })?;
+            Ok(())
         }
     }
 
@@ -572,24 +585,27 @@ pub mod referenced {
             range: R,
             collector: &mut Col,
             var_manager: &mut dyn ManageVars,
-        ) where
+        ) -> Result<(), crate::OutOfMemory>
+        where
             Col: CollectClauses,
             R: RangeBounds<usize>,
         {
             let range = super::super::prepare_ub_range(self, range);
             if range.is_empty() {
-                return;
+                return Ok(());
             }
-            let vals = self.db.borrow()[self.root.id].vals(
+            let mut vals = self.db.borrow()[self.root.id].vals(
                 self.root.rev_map_round_up(range.start + 1)
                     ..=self.root.rev_map(range.end + self.max_leaf_weight),
             );
-            vals.for_each(|val| {
+            vals.try_for_each(|val| {
                 self.db
                     .borrow_mut()
-                    .define_pos(self.root.id, val, collector, var_manager)
+                    .define_pos(self.root.id, val, collector, var_manager)?
                     .unwrap();
-            });
+                Ok::<(), crate::OutOfMemory>(())
+            })?;
+            Ok(())
         }
     }
 }
@@ -620,7 +636,8 @@ mod tests {
         gte.extend(lits);
         assert_eq!(gte.enforce_ub(4), Err(Error::NotEncoded));
         let mut var_manager = BasicVarManager::default();
-        gte.encode_ub(0..7, &mut Cnf::new(), &mut var_manager);
+        gte.encode_ub(0..7, &mut Cnf::new(), &mut var_manager)
+            .unwrap();
         assert_eq!(gte.depth(), 3);
         assert_eq!(gte.n_vars(), 10);
     }
@@ -636,13 +653,14 @@ mod tests {
         gte1.extend(lits.clone());
         let mut var_manager = BasicVarManager::default();
         let mut cnf1 = Cnf::new();
-        gte1.encode_ub(0..5, &mut cnf1, &mut var_manager);
+        gte1.encode_ub(0..5, &mut cnf1, &mut var_manager).unwrap();
         let mut gte2 = DbGte::default();
         gte2.extend(lits);
         let mut var_manager = BasicVarManager::default();
         let mut cnf2 = Cnf::new();
-        gte2.encode_ub(0..3, &mut cnf2, &mut var_manager);
-        gte2.encode_ub_change(0..5, &mut cnf2, &mut var_manager);
+        gte2.encode_ub(0..3, &mut cnf2, &mut var_manager).unwrap();
+        gte2.encode_ub_change(0..5, &mut cnf2, &mut var_manager)
+            .unwrap();
         assert_eq!(cnf1.len(), cnf2.len());
         assert_eq!(cnf1.len(), gte1.n_clauses());
         assert_eq!(cnf2.len(), gte2.n_clauses());
@@ -659,7 +677,7 @@ mod tests {
         gte1.extend(lits);
         let mut var_manager = BasicVarManager::default();
         let mut cnf1 = Cnf::new();
-        gte1.encode_ub(0..5, &mut cnf1, &mut var_manager);
+        gte1.encode_ub(0..5, &mut cnf1, &mut var_manager).unwrap();
         let mut gte2 = DbGte::default();
         let mut lits = RsHashMap::default();
         lits.insert(lit![0], 10);
@@ -669,7 +687,7 @@ mod tests {
         gte2.extend(lits);
         let mut var_manager = BasicVarManager::default();
         let mut cnf2 = Cnf::new();
-        gte2.encode_ub(0..9, &mut cnf2, &mut var_manager);
+        gte2.encode_ub(0..9, &mut cnf2, &mut var_manager).unwrap();
         assert_eq!(cnf1.len(), cnf2.len());
         assert_eq!(cnf1.len(), gte1.n_clauses());
         assert_eq!(cnf2.len(), gte2.n_clauses());
@@ -692,7 +710,8 @@ mod tests {
         lits.insert(lit![6], 1);
         gte.extend(lits);
         let mut gte_cnf = Cnf::new();
-        gte.encode_ub(3..8, &mut gte_cnf, &mut var_manager_gte);
+        gte.encode_ub(3..8, &mut gte_cnf, &mut var_manager_gte)
+            .unwrap();
         // Set up Tot
         let mut tot = card::Totalizer::default();
         tot.extend(vec![
@@ -705,7 +724,7 @@ mod tests {
             lit![6],
         ]);
         let mut tot_cnf = Cnf::new();
-        card::BoundUpper::encode_ub(&mut tot, 3..8, &mut tot_cnf, &mut var_manager_tot);
+        card::BoundUpper::encode_ub(&mut tot, 3..8, &mut tot_cnf, &mut var_manager_tot).unwrap();
         println!("{:?}", gte_cnf);
         println!("{:?}", tot_cnf);
         assert_eq!(var_manager_gte.new_var(), var_manager_tot.new_var());
diff --git a/rustsat/src/encodings/pb/dpw.rs b/rustsat/src/encodings/pb/dpw.rs
index 888c2b70..4ba90a46 100644
--- a/rustsat/src/encodings/pb/dpw.rs
+++ b/rustsat/src/encodings/pb/dpw.rs
@@ -130,7 +130,12 @@ impl EncodeIncremental for DynamicPolyWatchdog {
 }
 
 impl BoundUpper for DynamicPolyWatchdog {
-    fn encode_ub<Col, R>(&mut self, range: R, collector: &mut Col, var_manager: &mut dyn ManageVars)
+    fn encode_ub<Col, R>(
+        &mut self,
+        range: R,
+        collector: &mut Col,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<(), crate::OutOfMemory>
     where
         Col: CollectClauses,
         R: RangeBounds<usize>,
@@ -180,13 +185,14 @@ impl BoundUpperIncremental for DynamicPolyWatchdog {
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>,
     {
         let range = super::prepare_ub_range(self, range);
         if range.is_empty() || self.in_lits.len() <= 1 {
-            return;
+            return Ok(());
         }
         let n_vars_before = var_manager.n_used();
         if self.structure.is_none() && !self.in_lits.is_empty() {
@@ -202,13 +208,14 @@ impl BoundUpperIncremental for DynamicPolyWatchdog {
                 let output_weight = 1 << (structure.output_power());
                 let output_range = range.start / output_weight..(range.end - 1) / output_weight + 1;
                 for oidx in output_range {
-                    encode_output(structure, oidx, &mut self.db, collector, var_manager);
+                    encode_output(structure, oidx, &mut self.db, collector, var_manager)?;
                 }
                 self.n_clauses += collector.n_clauses() - n_clauses_before;
                 self.n_vars += var_manager.n_used() - n_vars_before;
             }
             None => (),
-        }
+        };
+        Ok(())
     }
 }
 
@@ -345,7 +352,8 @@ pub mod referenced {
             range: R,
             collector: &mut Col,
             var_manager: &mut dyn ManageVars,
-        ) where
+        ) -> Result<(), crate::OutOfMemory>
+        where
             Col: CollectClauses,
             R: RangeBounds<usize>,
         {
@@ -369,7 +377,8 @@ pub mod referenced {
             range: R,
             collector: &mut Col,
             var_manager: &mut dyn ManageVars,
-        ) where
+        ) -> Result<(), crate::OutOfMemory>
+        where
             Col: CollectClauses,
             R: RangeBounds<usize>,
         {
@@ -393,19 +402,21 @@ pub mod referenced {
             range: R,
             collector: &mut Col,
             var_manager: &mut dyn ManageVars,
-        ) where
+        ) -> Result<(), crate::OutOfMemory>
+        where
             Col: CollectClauses,
             R: RangeBounds<usize>,
         {
             let range = super::super::prepare_ub_range(self, range);
             if range.is_empty() {
-                return;
+                return Ok(());
             }
             let output_weight = 1 << self.structure.output_power();
             let output_range = range.start / output_weight..(range.end - 1) / output_weight + 1;
             for oidx in output_range {
-                encode_output(self.structure, oidx, self.db, collector, var_manager);
+                encode_output(self.structure, oidx, self.db, collector, var_manager)?;
             }
+            Ok(())
         }
     }
 
@@ -415,13 +426,14 @@ pub mod referenced {
             range: R,
             collector: &mut Col,
             var_manager: &mut dyn ManageVars,
-        ) where
+        ) -> Result<(), crate::OutOfMemory>
+        where
             Col: CollectClauses,
             R: RangeBounds<usize>,
         {
             let range = super::super::prepare_ub_range(self, range);
             if range.is_empty() {
-                return;
+                return Ok(());
             }
             let output_weight = 1 << self.structure.output_power();
             let output_range = range.start / output_weight..(range.end - 1) / output_weight + 1;
@@ -432,8 +444,9 @@ pub mod referenced {
                     &mut self.db.borrow_mut(),
                     collector,
                     var_manager,
-                );
+                )?;
             }
+            Ok(())
         }
     }
 }
@@ -586,13 +599,15 @@ fn encode_output<Col>(
     tot_db: &mut TotDb,
     collector: &mut Col,
     var_manager: &mut dyn ManageVars,
-) where
+) -> Result<(), crate::OutOfMemory>
+where
     Col: CollectClauses,
 {
     if oidx >= tot_db[dpw.root].max_val() {
-        return;
+        return Ok(());
     }
-    tot_db.define_pos_tot(dpw.root, oidx, collector, var_manager);
+    tot_db.define_pos_tot(dpw.root, oidx, collector, var_manager)?;
+    Ok(())
 }
 
 /// Enforces an upper bound value on a DPW [`Structure`]
@@ -649,7 +664,7 @@ mod tests {
         let mut dpw = DynamicPolyWatchdog::from(lits);
         let mut var_manager = BasicVarManager::from_next_free(Var::new(4));
         let mut cnf = Cnf::new();
-        dpw.encode_ub(0..=6, &mut cnf, &mut var_manager);
+        dpw.encode_ub(0..=6, &mut cnf, &mut var_manager).unwrap();
         assert_eq!(dpw.n_vars(), 9);
         assert_eq!(cnf.len(), 13);
     }
@@ -661,7 +676,7 @@ mod tests {
         let mut dpw = DynamicPolyWatchdog::from(lits);
         let mut var_manager = BasicVarManager::from_next_free(Var::new(1));
         let mut cnf = Cnf::new();
-        dpw.encode_ub(0..=6, &mut cnf, &mut var_manager);
+        dpw.encode_ub(0..=6, &mut cnf, &mut var_manager).unwrap();
         assert_eq!(dpw.n_vars(), 0);
         assert_eq!(cnf.len(), 0);
         debug_assert!(dpw.enforce_ub(4).unwrap().is_empty());
@@ -676,7 +691,7 @@ mod tests {
         let mut dpw = DynamicPolyWatchdog::from(lits);
         let mut var_manager = BasicVarManager::default();
         let mut cnf = Cnf::new();
-        dpw.encode_ub(0..=6, &mut cnf, &mut var_manager);
+        dpw.encode_ub(0..=6, &mut cnf, &mut var_manager).unwrap();
         assert_eq!(dpw.n_vars(), 0);
         assert_eq!(cnf.len(), 0);
         debug_assert!(dpw.enforce_ub(4).unwrap().is_empty());
@@ -693,7 +708,7 @@ mod tests {
         let mut dpw = DynamicPolyWatchdog::from(lits);
         let mut var_manager = BasicVarManager::default();
         let mut cnf = Cnf::new();
-        dpw.encode_ub(0..23, &mut cnf, &mut var_manager);
+        dpw.encode_ub(0..23, &mut cnf, &mut var_manager).unwrap();
         for ub in 7..23 {
             let coarse_ub = dpw.coarse_ub(ub);
             debug_assert!(coarse_ub <= ub);
@@ -715,7 +730,7 @@ mod tests {
         let mut dpw = DynamicPolyWatchdog::from(lits);
         let mut var_manager = BasicVarManager::default();
         let mut cnf = Cnf::new();
-        dpw.encode_ub(0..=4, &mut cnf, &mut var_manager);
+        dpw.encode_ub(0..=4, &mut cnf, &mut var_manager).unwrap();
         for ub in 0..4 {
             let coarse_ub = dpw.coarse_ub(ub);
             debug_assert_eq!(coarse_ub, ub);
diff --git a/rustsat/src/encodings/pb/gte.rs b/rustsat/src/encodings/pb/gte.rs
index 1ee15404..323ba6de 100644
--- a/rustsat/src/encodings/pb/gte.rs
+++ b/rustsat/src/encodings/pb/gte.rs
@@ -154,14 +154,19 @@ impl EncodeIncremental for GeneralizedTotalizer {
 }
 
 impl BoundUpper for GeneralizedTotalizer {
-    fn encode_ub<Col, R>(&mut self, range: R, collector: &mut Col, var_manager: &mut dyn ManageVars)
+    fn encode_ub<Col, R>(
+        &mut self,
+        range: R,
+        collector: &mut Col,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<(), crate::OutOfMemory>
     where
         Col: CollectClauses,
         R: RangeBounds<usize>,
     {
         let range = super::prepare_ub_range(self, range);
         if range.is_empty() {
-            return;
+            return Ok(());
         };
         let n_vars_before = var_manager.n_used();
         let n_clauses_before = collector.n_clauses();
@@ -172,10 +177,11 @@ impl BoundUpper for GeneralizedTotalizer {
                 range.start + 1..range.end + self.max_leaf_weight + 1,
                 collector,
                 var_manager,
-            ),
+            )?,
         };
         self.n_clauses += collector.n_clauses() - n_clauses_before;
         self.n_vars += var_manager.n_used() - n_vars_before;
+        Ok(())
     }
 
     fn enforce_ub(&self, ub: usize) -> Result<Vec<Lit>, Error> {
@@ -236,13 +242,14 @@ impl BoundUpperIncremental for GeneralizedTotalizer {
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>,
     {
         let range = super::prepare_ub_range(self, range);
         if range.is_empty() {
-            return;
+            return Ok(());
         };
         let n_vars_before = var_manager.n_used();
         let n_clauses_before = collector.n_clauses();
@@ -252,10 +259,11 @@ impl BoundUpperIncremental for GeneralizedTotalizer {
                 range.start + 1..range.end + self.max_leaf_weight,
                 collector,
                 var_manager,
-            );
+            )?;
         }
         self.n_clauses += collector.n_clauses() - n_clauses_before;
         self.n_vars += var_manager.n_used() - n_vars_before;
+        Ok(())
     }
 }
 
@@ -412,12 +420,13 @@ impl Node {
         range: Range<usize>,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
     {
         let range = self.limit_range(range);
         if range.is_empty() {
-            return;
+            return Ok(());
         }
 
         // Reserve vars if needed
@@ -436,19 +445,17 @@ impl Node {
                 let right_lits = right.lit_map(&mut right_tmp_map);
                 // Encode adder for current node
                 // Propagate left value
-                for (&left_val, &left_lit) in left_lits.range(range.clone()) {
-                    collector.extend([atomics::lit_impl_lit(
-                        left_lit,
-                        *out_lits.get(&left_val).unwrap(),
-                    )]);
-                }
+                collector.extend_clauses(left_lits.range(range.clone()).map(
+                    |(left_val, &left_lit)| {
+                        atomics::lit_impl_lit(left_lit, *out_lits.get(left_val).unwrap())
+                    },
+                ))?;
                 // Propagate right value
-                for (&right_val, &right_lit) in right_lits.range(range.clone()) {
-                    collector.extend([atomics::lit_impl_lit(
-                        right_lit,
-                        *out_lits.get(&right_val).unwrap(),
-                    )]);
-                }
+                collector.extend_clauses(right_lits.range(range.clone()).map(
+                    |(right_val, &right_lit)| {
+                        atomics::lit_impl_lit(right_lit, *out_lits.get(right_val).unwrap())
+                    },
+                ))?;
                 // Propagate sum
                 if range.end > 1 {
                     let clause_from_data =
@@ -479,10 +486,11 @@ impl Node {
                                         clause_from_data(left_val, right_val, left_lit, right_lit)
                                     })
                             });
-                    collector.extend(clause_iter);
+                    collector.extend_clauses(clause_iter)?;
                 }
             }
-        }
+        };
+        Ok(())
     }
 
     /// Encodes the output literals from the children to this node in a given
@@ -493,12 +501,13 @@ impl Node {
         range: Range<usize>,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
     {
         let range = self.limit_range(range);
         if range.is_empty() {
-            return;
+            return Ok(());
         }
 
         // Ignore all previous encoding and encode from scratch
@@ -508,16 +517,18 @@ impl Node {
                 let left_range = Node::compute_required_min_enc(range.clone(), right.max_val());
                 let right_range = Node::compute_required_min_enc(range.clone(), left.max_val());
                 // Recurse
-                left.rec_encode(left_range, collector, var_manager);
-                right.rec_encode(right_range, collector, var_manager);
+                left.rec_encode(left_range, collector, var_manager)?;
+                right.rec_encode(right_range, collector, var_manager)?;
 
                 // Encode current node
                 let n_clauses_before = collector.n_clauses();
-                self.encode_range(range.clone(), collector, var_manager);
+                self.encode_range(range.clone(), collector, var_manager)?;
 
                 self.update_stats(range, collector.n_clauses() - n_clauses_before);
             }
-        }
+        };
+
+        Ok(())
     }
 
     /// Encodes the output literals from the children to this node in a given
@@ -527,12 +538,13 @@ impl Node {
         range: Range<usize>,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
     {
         let range = self.limit_range(range);
         if range.is_empty() {
-            return;
+            return Ok(());
         }
 
         match self {
@@ -549,27 +561,28 @@ impl Node {
                 let left_range = Node::compute_required_min_enc(range.clone(), right.max_val());
                 let right_range = Node::compute_required_min_enc(range.clone(), left.max_val());
                 // Recurse
-                left.rec_encode_change(left_range, collector, var_manager);
-                right.rec_encode_change(right_range, collector, var_manager);
+                left.rec_encode_change(left_range, collector, var_manager)?;
+                right.rec_encode_change(right_range, collector, var_manager)?;
 
                 // Encode changes for current node
                 let n_clauses_before = collector.n_clauses();
                 if enc_range.is_empty() {
                     // First time encoding this node
-                    self.encode_range(range.clone(), collector, var_manager);
+                    self.encode_range(range.clone(), collector, var_manager)?;
                 } else {
                     // Partially encoded
                     if range.start < enc_range.start {
-                        self.encode_range(range.start..enc_range.start, collector, var_manager);
+                        self.encode_range(range.start..enc_range.start, collector, var_manager)?;
                     };
                     if range.end > enc_range.end {
-                        self.encode_range(enc_range.end..range.end, collector, var_manager);
+                        self.encode_range(enc_range.end..range.end, collector, var_manager)?;
                     };
                 };
 
                 self.update_stats(range, collector.n_clauses() - n_clauses_before);
             }
-        }
+        };
+        Ok(())
     }
 
     /// Reserves variables this node might need in a given range
@@ -715,7 +728,7 @@ mod tests {
         let mut node = Node::new_internal(child1, child2);
         let mut var_manager = BasicVarManager::default();
         let mut cnf = Cnf::new();
-        node.encode_range(0..9, &mut cnf, &mut var_manager);
+        node.encode_range(0..9, &mut cnf, &mut var_manager).unwrap();
         match &node {
             Node::Leaf { .. } => panic!(),
             Node::Internal { out_lits, .. } => assert_eq!(out_lits.len(), 3),
@@ -757,7 +770,7 @@ mod tests {
         let mut node = Node::new_internal(child1, child2);
         let mut var_manager = BasicVarManager::default();
         let mut cnf = Cnf::new();
-        node.encode_range(0..7, &mut cnf, &mut var_manager);
+        node.encode_range(0..7, &mut cnf, &mut var_manager).unwrap();
         match &node {
             Node::Leaf { .. } => panic!(),
             Node::Internal { out_lits, .. } => assert_eq!(out_lits.len(), 3),
@@ -799,7 +812,7 @@ mod tests {
         let mut node = Node::new_internal(child1, child2);
         let mut var_manager = BasicVarManager::default();
         let mut cnf = Cnf::new();
-        node.encode_range(4..7, &mut cnf, &mut var_manager);
+        node.encode_range(4..7, &mut cnf, &mut var_manager).unwrap();
         match &node {
             Node::Leaf { .. } => panic!(),
             Node::Internal { out_lits, .. } => assert_eq!(out_lits.len(), 2),
@@ -841,7 +854,7 @@ mod tests {
         let mut node = Node::new_internal(child1, child2);
         let mut var_manager = BasicVarManager::default();
         let mut cnf = Cnf::new();
-        node.encode_range(6..5, &mut cnf, &mut var_manager);
+        node.encode_range(6..5, &mut cnf, &mut var_manager).unwrap();
         assert_eq!(cnf.len(), 0);
     }
 
@@ -856,7 +869,8 @@ mod tests {
         gte.extend(lits);
         assert_eq!(gte.enforce_ub(4), Err(Error::NotEncoded));
         let mut var_manager = BasicVarManager::default();
-        gte.encode_ub(0..7, &mut Cnf::new(), &mut var_manager);
+        gte.encode_ub(0..7, &mut Cnf::new(), &mut var_manager)
+            .unwrap();
         assert_eq!(gte.depth(), 3);
         assert_eq!(gte.n_vars(), 10);
     }
@@ -872,13 +886,14 @@ mod tests {
         gte1.extend(lits.clone());
         let mut var_manager = BasicVarManager::default();
         let mut cnf1 = Cnf::new();
-        gte1.encode_ub(0..5, &mut cnf1, &mut var_manager);
+        gte1.encode_ub(0..5, &mut cnf1, &mut var_manager).unwrap();
         let mut gte2 = GeneralizedTotalizer::default();
         gte2.extend(lits);
         let mut var_manager = BasicVarManager::default();
         let mut cnf2 = Cnf::new();
-        gte2.encode_ub(0..3, &mut cnf2, &mut var_manager);
-        gte2.encode_ub_change(0..5, &mut cnf2, &mut var_manager);
+        gte2.encode_ub(0..3, &mut cnf2, &mut var_manager).unwrap();
+        gte2.encode_ub_change(0..5, &mut cnf2, &mut var_manager)
+            .unwrap();
         assert_eq!(cnf1.len(), cnf2.len());
         assert_eq!(cnf1.len(), gte1.n_clauses());
         assert_eq!(cnf2.len(), gte2.n_clauses());
@@ -895,7 +910,7 @@ mod tests {
         gte1.extend(lits);
         let mut var_manager = BasicVarManager::default();
         let mut cnf1 = Cnf::new();
-        gte1.encode_ub(0..5, &mut cnf1, &mut var_manager);
+        gte1.encode_ub(0..5, &mut cnf1, &mut var_manager).unwrap();
         let mut gte2 = GeneralizedTotalizer::default();
         let mut lits = RsHashMap::default();
         lits.insert(lit![0], 10);
@@ -905,7 +920,7 @@ mod tests {
         gte2.extend(lits);
         let mut var_manager = BasicVarManager::default();
         let mut cnf2 = Cnf::new();
-        gte2.encode_ub(0..9, &mut cnf2, &mut var_manager);
+        gte2.encode_ub(0..9, &mut cnf2, &mut var_manager).unwrap();
         assert_eq!(cnf1.len(), cnf2.len());
         assert_eq!(cnf1.len(), gte1.n_clauses());
         assert_eq!(cnf2.len(), gte2.n_clauses());
@@ -928,7 +943,8 @@ mod tests {
         lits.insert(lit![6], 1);
         gte.extend(lits);
         let mut gte_cnf = Cnf::new();
-        gte.encode_ub(3..8, &mut gte_cnf, &mut var_manager_gte);
+        gte.encode_ub(3..8, &mut gte_cnf, &mut var_manager_gte)
+            .unwrap();
         // Set up Tot
         let mut tot = card::Totalizer::default();
         tot.extend(vec![
@@ -941,7 +957,7 @@ mod tests {
             lit![6],
         ]);
         let mut tot_cnf = Cnf::new();
-        card::BoundUpper::encode_ub(&mut tot, 3..8, &mut tot_cnf, &mut var_manager_tot);
+        card::BoundUpper::encode_ub(&mut tot, 3..8, &mut tot_cnf, &mut var_manager_tot).unwrap();
         println!("{:?}", gte_cnf);
         println!("{:?}", tot_cnf);
         assert_eq!(var_manager_gte.new_var(), var_manager_tot.new_var());
diff --git a/rustsat/src/encodings/pb/simulators.rs b/rustsat/src/encodings/pb/simulators.rs
index 022d9578..20528062 100644
--- a/rustsat/src/encodings/pb/simulators.rs
+++ b/rustsat/src/encodings/pb/simulators.rs
@@ -132,7 +132,12 @@ impl<PBE> BoundUpper for Inverted<PBE>
 where
     PBE: BoundLower,
 {
-    fn encode_ub<Col, R>(&mut self, range: R, collector: &mut Col, var_manager: &mut dyn ManageVars)
+    fn encode_ub<Col, R>(
+        &mut self,
+        range: R,
+        collector: &mut Col,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<(), crate::OutOfMemory>
     where
         Col: CollectClauses,
         R: RangeBounds<usize>,
@@ -158,7 +163,12 @@ impl<PBE> BoundLower for Inverted<PBE>
 where
     PBE: BoundUpper,
 {
-    fn encode_lb<Col, R>(&mut self, range: R, collector: &mut Col, var_manager: &mut dyn ManageVars)
+    fn encode_lb<Col, R>(
+        &mut self,
+        range: R,
+        collector: &mut Col,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<(), crate::OutOfMemory>
     where
         Col: CollectClauses,
         R: RangeBounds<usize>,
@@ -189,7 +199,8 @@ where
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>,
     {
@@ -210,7 +221,8 @@ where
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>,
     {
@@ -347,7 +359,12 @@ where
     UBE: BoundUpper,
     LBE: BoundLower,
 {
-    fn encode_ub<Col, R>(&mut self, range: R, collector: &mut Col, var_manager: &mut dyn ManageVars)
+    fn encode_ub<Col, R>(
+        &mut self,
+        range: R,
+        collector: &mut Col,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<(), crate::OutOfMemory>
     where
         Col: CollectClauses,
         R: RangeBounds<usize>,
@@ -365,7 +382,12 @@ where
     UBE: BoundUpper,
     LBE: BoundLower,
 {
-    fn encode_lb<Col, R>(&mut self, range: R, collector: &mut Col, var_manager: &mut dyn ManageVars)
+    fn encode_lb<Col, R>(
+        &mut self,
+        range: R,
+        collector: &mut Col,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<(), crate::OutOfMemory>
     where
         Col: CollectClauses,
         R: RangeBounds<usize>,
@@ -388,7 +410,8 @@ where
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>,
     {
@@ -406,7 +429,8 @@ where
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>,
     {
@@ -529,7 +553,12 @@ impl<CE> BoundUpper for Card<CE>
 where
     CE: card::BoundUpper,
 {
-    fn encode_ub<Col, R>(&mut self, range: R, collector: &mut Col, var_manager: &mut dyn ManageVars)
+    fn encode_ub<Col, R>(
+        &mut self,
+        range: R,
+        collector: &mut Col,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<(), crate::OutOfMemory>
     where
         Col: CollectClauses,
         R: RangeBounds<usize>,
@@ -546,7 +575,12 @@ impl<CE> BoundLower for Card<CE>
 where
     CE: card::BoundLower,
 {
-    fn encode_lb<Col, R>(&mut self, range: R, collector: &mut Col, var_manager: &mut dyn ManageVars)
+    fn encode_lb<Col, R>(
+        &mut self,
+        range: R,
+        collector: &mut Col,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<(), crate::OutOfMemory>
     where
         Col: CollectClauses,
         R: RangeBounds<usize>,
@@ -568,7 +602,8 @@ where
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>,
     {
@@ -586,7 +621,8 @@ where
         range: R,
         collector: &mut Col,
         var_manager: &mut dyn ManageVars,
-    ) where
+    ) -> Result<(), crate::OutOfMemory>
+    where
         Col: CollectClauses,
         R: RangeBounds<usize>,
     {
diff --git a/rustsat/src/instances/multiopt.rs b/rustsat/src/instances/multiopt.rs
index ce0e56dd..ff95748e 100644
--- a/rustsat/src/instances/multiopt.rs
+++ b/rustsat/src/instances/multiopt.rs
@@ -149,6 +149,10 @@ impl<VM: ManageVars> MultiOptInstance<VM> {
     }
 
     /// Converts the instance to a set of hard and soft clauses
+    ///
+    /// # Panic
+    ///
+    /// This might panic if the conversion to [`Cnf`] runs out of memory.
     pub fn into_hard_cls_soft_cls(self) -> (Cnf, Vec<(impl WClsIter, isize)>, VM) {
         let (cnf, mut vm) = self.constrs.into_cnf();
         let omv = self.objs.iter().fold(Var::new(0), |v, o| {
@@ -172,6 +176,10 @@ impl<VM: ManageVars> MultiOptInstance<VM> {
     }
 
     /// Converts the instance to a set of hard clauses and soft literals
+    ///
+    /// # Panic
+    ///
+    /// This might panic if the conversion to [`Cnf`] runs out of memory.
     pub fn into_hard_cls_soft_lits(self) -> (Cnf, Vec<(impl WLitIter, isize)>, VM) {
         let (mut cnf, mut vm) = self.constrs.into_cnf();
         let omv = self.objs.iter().fold(Var::new(0), |v, o| {
@@ -245,8 +253,14 @@ impl<VM: ManageVars> MultiOptInstance<VM> {
     pub fn to_dimacs<W: io::Write>(self, writer: &mut W) -> Result<(), io::Error> {
         #[allow(deprecated)]
         self.to_dimacs_with_encoders(
-            card::default_encode_cardinality_constraint,
-            pb::default_encode_pb_constraint,
+            |constr, cnf, vm| {
+                card::default_encode_cardinality_constraint(constr, cnf, vm)
+                    .expect("cardinality encoding ran out of memory")
+            },
+            |constr, cnf, vm| {
+                pb::default_encode_pb_constraint(constr, cnf, vm)
+                    .expect("pb encoding ran out of memory")
+            },
             writer,
         )
     }
diff --git a/rustsat/src/instances/opt.rs b/rustsat/src/instances/opt.rs
index 86c439d3..9c6854aa 100644
--- a/rustsat/src/instances/opt.rs
+++ b/rustsat/src/instances/opt.rs
@@ -1102,6 +1102,10 @@ impl<VM: ManageVars> OptInstance<VM> {
 
     /// Converts the instance to a set of hard and soft clauses, an objective
     /// offset and a variable manager
+    ///
+    /// # Panic
+    ///
+    /// This might panic if the conversion to [`Cnf`] runs out of memory.
     pub fn into_hard_cls_soft_cls(self) -> (Cnf, (impl WClsIter, isize), VM) {
         let (cnf, mut vm) = self.constrs.into_cnf();
         if let Some(mv) = self.obj.max_var() {
@@ -1112,6 +1116,10 @@ impl<VM: ManageVars> OptInstance<VM> {
 
     /// Converts the instance to a set of hard clauses and soft literals, an
     /// objective offset and a variable manager
+    ///
+    /// # Panic
+    ///
+    /// This might panic if the conversion to [`Cnf`] runs out of memory.
     pub fn into_hard_cls_soft_lits(self) -> (Cnf, (impl WLitIter, isize), VM) {
         let (mut cnf, mut vm) = self.constrs.into_cnf();
         if let Some(mv) = self.obj.max_var() {
@@ -1170,8 +1178,14 @@ impl<VM: ManageVars> OptInstance<VM> {
     pub fn to_dimacs<W: io::Write>(self, writer: &mut W) -> Result<(), io::Error> {
         #[allow(deprecated)]
         self.to_dimacs_with_encoders(
-            card::default_encode_cardinality_constraint,
-            pb::default_encode_pb_constraint,
+            |constr, cnf, vm| {
+                card::default_encode_cardinality_constraint(constr, cnf, vm)
+                    .expect("cardinality encoding ran out of memory")
+            },
+            |constr, cnf, vm| {
+                pb::default_encode_pb_constraint(constr, cnf, vm)
+                    .expect("pb encoding ran out of memory")
+            },
             writer,
         )
     }
diff --git a/rustsat/src/instances/sat.rs b/rustsat/src/instances/sat.rs
index b765983e..e2d9ac31 100644
--- a/rustsat/src/instances/sat.rs
+++ b/rustsat/src/instances/sat.rs
@@ -1,6 +1,6 @@
 //! # Satsifiability Instance Representations
 
-use std::{collections::TryReserveError, io, ops::Index, path::Path};
+use std::{cmp, collections::TryReserveError, io, ops::Index, path::Path};
 
 use crate::{
     clause,
@@ -10,6 +10,7 @@ use crate::{
         constraints::{CardConstraint, PBConstraint},
         Assignment, Clause, Lit, Var,
     },
+    utils::LimitedIter,
     RequiresClausal,
 };
 
@@ -217,6 +218,28 @@ impl CollectClauses for Cnf {
     fn n_clauses(&self) -> usize {
         self.clauses.len()
     }
+
+    fn extend_clauses<T>(&mut self, cl_iter: T) -> Result<(), crate::OutOfMemory>
+    where
+        T: IntoIterator<Item = Clause>,
+    {
+        let cl_iter = cl_iter.into_iter();
+        if let Some(ub) = cl_iter.size_hint().1 {
+            self.try_reserve(ub)?;
+            self.extend(cl_iter);
+        } else {
+            // Extend by reserving in exponential chunks
+            let mut cl_iter = cl_iter.peekable();
+            while cl_iter.peek().is_some() {
+                let additional = (self.len() + cmp::max(cl_iter.size_hint().0, 1))
+                    .next_power_of_two()
+                    - self.len();
+                self.try_reserve(additional)?;
+                self.extend(LimitedIter::new(&mut cl_iter, additional));
+            }
+        }
+        Ok(())
+    }
 }
 
 impl IntoIterator for Cnf {
@@ -505,10 +528,20 @@ impl<VM: ManageVars> SatInstance<VM> {
     /// Uses the default encoders from the `encodings` module.
     ///
     /// See [`Self::convert_to_cnf`] for converting in place
+    ///
+    /// # Panic
+    ///
+    /// This might panic if the conversion to [`Cnf`] runs out of memory.
     pub fn into_cnf(self) -> (Cnf, VM) {
         self.into_cnf_with_encoders(
-            card::default_encode_cardinality_constraint,
-            pb::default_encode_pb_constraint,
+            |constr, cnf, vm| {
+                card::default_encode_cardinality_constraint(constr, cnf, vm)
+                    .expect("cardinality encoding ran out of memory")
+            },
+            |constr, cnf, vm| {
+                pb::default_encode_pb_constraint(constr, cnf, vm)
+                    .expect("pb encoding ran out of memory")
+            },
         )
     }
 
@@ -516,10 +549,20 @@ impl<VM: ManageVars> SatInstance<VM> {
     /// Uses the default encoders from the `encodings` module.
     ///
     /// See [`Self::into_cnf`] if you don't need to convert in place
+    ///
+    /// # Panic
+    ///
+    /// This might panic if the conversion to [`Cnf`] runs out of memory.
     pub fn convert_to_cnf(&mut self) {
         self.convert_to_cnf_with_encoders(
-            card::default_encode_cardinality_constraint,
-            pb::default_encode_pb_constraint,
+            |constr, cnf, vm| {
+                card::default_encode_cardinality_constraint(constr, cnf, vm)
+                    .expect("cardinality encoding ran out of memory")
+            },
+            |constr, cnf, vm| {
+                pb::default_encode_pb_constraint(constr, cnf, vm)
+                    .expect("pb encoding ran out of memory")
+            },
         )
     }
 
@@ -545,6 +588,10 @@ impl<VM: ManageVars> SatInstance<VM> {
     /// converters for non-clausal constraints.
     ///
     /// See [`Self::into_cnf_with_encoders`] to convert in place
+    ///
+    /// # Panic
+    ///
+    /// The encoder functions might panic if the conversion runs out of memory.
     pub fn into_cnf_with_encoders<CardEnc, PBEnc>(
         mut self,
         card_encoder: CardEnc,
@@ -562,6 +609,10 @@ impl<VM: ManageVars> SatInstance<VM> {
     /// converters for non-clausal constraints.
     ///
     /// See [`Self::into_cnf_with_encoders`] if you don't need to convert in place
+    ///
+    /// # Panic
+    ///
+    /// The encoder functions might panic if the conversion runs out of memory.
     pub fn convert_to_cnf_with_encoders<CardEnc, PBEnc>(
         &mut self,
         mut card_encoder: CardEnc,
@@ -632,8 +683,14 @@ impl<VM: ManageVars> SatInstance<VM> {
     pub fn to_dimacs<W: io::Write>(self, writer: &mut W) -> Result<(), io::Error> {
         #[allow(deprecated)]
         self.to_dimacs_with_encoders(
-            card::default_encode_cardinality_constraint,
-            pb::default_encode_pb_constraint,
+            |constr, cnf, vm| {
+                card::default_encode_cardinality_constraint(constr, cnf, vm)
+                    .expect("cardinality encoding ran out of memory")
+            },
+            |constr, cnf, vm| {
+                pb::default_encode_pb_constraint(constr, cnf, vm)
+                    .expect("pb encoding ran out of memory")
+            },
             writer,
         )
     }
@@ -944,3 +1001,16 @@ impl<VM: ManageVars + Default> From<Cnf> for SatInstance<VM> {
         inst
     }
 }
+
+impl CollectClauses for SatInstance {
+    fn n_clauses(&self) -> usize {
+        self.n_clauses()
+    }
+
+    fn extend_clauses<T>(&mut self, cl_iter: T) -> Result<(), crate::OutOfMemory>
+    where
+        T: IntoIterator<Item = Clause>,
+    {
+        self.cnf.extend_clauses(cl_iter)
+    }
+}
diff --git a/rustsat/src/lib.rs b/rustsat/src/lib.rs
index eb075db9..e212494c 100644
--- a/rustsat/src/lib.rs
+++ b/rustsat/src/lib.rs
@@ -67,6 +67,7 @@
 #![warn(missing_docs)]
 
 use core::fmt;
+use std::collections::TryReserveError;
 
 use thiserror::Error;
 
@@ -93,6 +94,28 @@ impl fmt::Display for NotAllowed {
 #[cfg(test)]
 mod bench;
 
+/// Error returned when an operation ran out of memory
+///
+/// The library is not _fully_ memory safe, meaning there are cases where memory allocation failing
+/// can lead to a panic instead to an error. Mainly add clauses to solvers and collecting clauses
+/// from encodings are done in a safe way. This is intended, e.g., for anytime solvers that might
+/// want a change to print a final output if they run out of memory.
+#[derive(Error, Debug, PartialEq, Eq)]
+pub enum OutOfMemory {
+    /// A `try_reserve` operation in Rust ran out of memory
+    #[error("try reserve error: {0}")]
+    TryReserve(TryReserveError),
+    /// An external API (typically a solver) ran out of memory
+    #[error("external API operation ran out of memory")]
+    ExternalApi,
+}
+
+impl From<TryReserveError> for OutOfMemory {
+    fn from(value: TryReserveError) -> Self {
+        OutOfMemory::TryReserve(value)
+    }
+}
+
 /// Error returned if an operation requires clausal constraints, but this is not the case
 #[derive(Error, Debug)]
 #[error("operation requires a clausal constraint(s) but it is not")]
diff --git a/rustsat/src/solvers.rs b/rustsat/src/solvers.rs
index 7707a4da..c0aefc2c 100644
--- a/rustsat/src/solvers.rs
+++ b/rustsat/src/solvers.rs
@@ -469,8 +469,34 @@ impl fmt::Display for StateError {
     }
 }
 
+macro_rules! pass_oom_or_panic {
+    ($result:expr) => {{
+        match $result {
+            Ok(res) => res,
+            Err(err) => match err.downcast::<crate::OutOfMemory>() {
+                Ok(oom) => return Err(oom),
+                Err(err) => panic!("unexpected error in clause collector: {err}"),
+            },
+        }
+    }};
+}
+
 impl<S: Solve + SolveStats> CollectClauses for S {
     fn n_clauses(&self) -> usize {
         self.n_clauses()
     }
+
+    fn extend_clauses<T>(&mut self, cl_iter: T) -> Result<(), crate::OutOfMemory>
+    where
+        T: IntoIterator<Item = Clause>,
+    {
+        for cl in cl_iter {
+            pass_oom_or_panic!(self.add_clause(cl));
+        }
+        Ok(())
+    }
+
+    fn add_clause(&mut self, cl: Clause) -> Result<(), crate::OutOfMemory> {
+        Ok(pass_oom_or_panic!(self.add_clause(cl)))
+    }
 }
diff --git a/rustsat/src/utils.rs b/rustsat/src/utils.rs
index f2732e54..d0875651 100644
--- a/rustsat/src/utils.rs
+++ b/rustsat/src/utils.rs
@@ -32,6 +32,36 @@ pub(crate) fn digits(mut number: usize, mut basis: u8) -> u32 {
     digits
 }
 
+/// A wrapper around an iterator to only yield a limited number of elements and then stop
+///
+/// As opposed to [`std::iter::Take`] this does not take ownership of the original iterator
+pub struct LimitedIter<'iter, I> {
+    iter: &'iter mut I,
+    remaining: usize,
+}
+
+impl<'iter, I> LimitedIter<'iter, I> {
+    /// Creates a new iterator that yields at most `remaining` elements
+    pub fn new(iter: &'iter mut I, remaining: usize) -> Self {
+        Self { iter, remaining }
+    }
+}
+
+impl<I> Iterator for LimitedIter<'_, I>
+where
+    I: Iterator,
+{
+    type Item = <I as Iterator>::Item;
+
+    fn next(&mut self) -> Option<Self::Item> {
+        if self.remaining == 0 {
+            return None;
+        }
+        self.remaining -= 1;
+        self.iter.next()
+    }
+}
+
 #[cfg(test)]
 mod tests {
     #[test]


Test patch:
diff --git a/cadical/test-all.sh b/cadical/test-all.sh
index afdfed3c..c706bde8 100755
--- a/cadical/test-all.sh
+++ b/cadical/test-all.sh
@@ -1,97 +1,121 @@
 #!/usr/bin/bash
 
 echo "Testing default (newest) version"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test &> def-test.log
 echo "Default (newest) test returned: $?"
 
 echo "Testing v1.5.0"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=v1-5-0 &> v150-test.log
 echo "v1.5.0 test returned: $?"
 
 echo "Testing v1.5.1"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=v1-5-1 &> v151-test.log
 echo "v1.5.1 test returned: $?"
 
 echo "Testing v1.5.2"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=v1-5-2 &> v152-test.log
 echo "v1.5.2 test returned: $?"
 
 echo "Testing v1.5.3"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=v1-5-3 &> v153-test.log
 echo "v1.5.3 test returned: $?"
 
 echo "Testing v1.5.4"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=v1-5-4 &> v154-test.log
 echo "v1.5.4 test returned: $?"
 
 echo "Testing v1.5.5"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=v1-5-5 &> v155-test.log
 echo "v1.5.5 test returned: $?"
 
 echo "Testing v1.5.6"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=v1-5-6 &> v156-test.log
 echo "v1.5.6 test returned: $?"
 
 echo "Testing v1.6.0"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=v1-6-0 &> v160-test.log
 echo "v1.6.0 test returned: $?"
 
 echo "Testing v1.7.0"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=v1-7-0 &> v170-test.log
 echo "v1.7.0 test returned: $?"
 
 echo "Testing v1.7.1"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=v1-7-1 &> v171-test.log
 echo "v1.7.1 test returned: $?"
 
 echo "Testing v1.7.2"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=v1-7-2 &> v172-test.log
 echo "v1.7.2 test returned: $?"
 
 echo "Testing v1.7.3"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=v1-7-3 &> v173-test.log
 echo "v1.7.3 test returned: $?"
 
 echo "Testing v1.7.4"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=v1-7-4 &> v174-test.log
 echo "v1.7.4 test returned: $?"
 
 echo "Testing v1.7.5"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=v1-7-5 &> v175-test.log
 echo "v1.7.5 test returned: $?"
 
 echo "Testing v1.8.0"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=v1-8-0 &> v180-test.log
 echo "v1.8.0 test returned: $?"
 
 echo "Testing v1.9.0"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=v1-9-0 &> v190-test.log
 echo "v1.9.0 test returned: $?"
 
 echo "Testing v1.9.1"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=v1-9-1 &> v191-test.log
 echo "v1.9.1 test returned: $?"
 
 echo "Testing v1.9.2"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=v1-9-2 &> v192-test.log
 echo "v1.9.2 test returned: $?"
 
 echo "Testing v1.9.3"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=v1-9-3 &> v193-test.log
 echo "v1.9.3 test returned: $?"
 
 echo "Testing v1.9.4"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=v1-9-4 &> v194-test.log
 echo "v1.9.4 test returned: $?"
 
 echo "Testing v1.9.5"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=v1-9-5 &> v195-test.log
 echo "v1.9.5 test returned: $?"
 
 echo "Testing quiet"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=quiet &> quiet-test.log
 echo "quiet test returned: $?"
 
 echo "Testing logging"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=logging &> logging-test.log
 echo "logging test returned: $?"
diff --git a/rustsat/tests/card_encodings.rs b/rustsat/tests/card_encodings.rs
index 1b5e3af3..ba31a267 100644
--- a/rustsat/tests/card_encodings.rs
+++ b/rustsat/tests/card_encodings.rs
@@ -39,7 +39,8 @@ fn test_inc_both_card<CE: BoundBothIncremental + Extend<Lit> + Default>() {
     let mut enc = CE::default();
     enc.extend(vec![lit![0], lit![1], lit![2], lit![3], lit![4]]);
 
-    enc.encode_both(2..3, &mut solver, &mut var_manager);
+    enc.encode_both(2..3, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_lb(2).unwrap();
     let res = solver.solve_assumps(&assumps).unwrap();
     assert_eq!(res, SolverResult::Sat);
@@ -48,31 +49,36 @@ fn test_inc_both_card<CE: BoundBothIncremental + Extend<Lit> + Default>() {
     let res = solver.solve_assumps(&assumps).unwrap();
     assert_eq!(res, SolverResult::Unsat);
 
-    enc.encode_both_change(0..4, &mut solver, &mut var_manager);
+    enc.encode_both_change(0..4, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_ub(3).unwrap();
     let res = solver.solve_assumps(&assumps).unwrap();
     assert_eq!(res, SolverResult::Sat);
 
     enc.extend(vec![lit![5]]);
 
-    enc.encode_both_change(0..4, &mut solver, &mut var_manager);
+    enc.encode_both_change(0..4, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_ub(3).unwrap();
     let res = solver.solve_assumps(&assumps).unwrap();
     assert_eq!(res, SolverResult::Unsat);
 
-    enc.encode_both_change(0..5, &mut solver, &mut var_manager);
+    enc.encode_both_change(0..5, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_ub(4).unwrap();
     let res = solver.solve_assumps(&assumps).unwrap();
     assert_eq!(res, SolverResult::Sat);
 
     enc.extend(vec![lit![6], lit![7], lit![8], lit![9], lit![10]]);
 
-    enc.encode_both_change(0..5, &mut solver, &mut var_manager);
+    enc.encode_both_change(0..5, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_ub(4).unwrap();
     let res = solver.solve_assumps(&assumps).unwrap();
     assert_eq!(res, SolverResult::Unsat);
 
-    enc.encode_both_change(0..8, &mut solver, &mut var_manager);
+    enc.encode_both_change(0..8, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_ub(7).unwrap();
     let res = solver.solve_assumps(&assumps).unwrap();
     assert_eq!(res, SolverResult::Sat);
@@ -103,36 +109,41 @@ fn test_inc_ub_card<CE: BoundUpperIncremental + Extend<Lit> + Default>() {
     let mut enc = CE::default();
     enc.extend(vec![lit![0], lit![1], lit![2], lit![3], lit![4]]);
 
-    enc.encode_ub(2..3, &mut solver, &mut var_manager);
+    enc.encode_ub(2..3, &mut solver, &mut var_manager).unwrap();
     let assumps = enc.enforce_ub(2).unwrap();
     let res = solver.solve_assumps(&assumps).unwrap();
     assert_eq!(res, SolverResult::Unsat);
 
-    enc.encode_ub_change(0..4, &mut solver, &mut var_manager);
+    enc.encode_ub_change(0..4, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_ub(3).unwrap();
     let res = solver.solve_assumps(&assumps).unwrap();
     assert_eq!(res, SolverResult::Sat);
 
     enc.extend(vec![lit![5]]);
 
-    enc.encode_ub_change(0..4, &mut solver, &mut var_manager);
+    enc.encode_ub_change(0..4, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_ub(3).unwrap();
     let res = solver.solve_assumps(&assumps).unwrap();
     assert_eq!(res, SolverResult::Unsat);
 
-    enc.encode_ub_change(0..5, &mut solver, &mut var_manager);
+    enc.encode_ub_change(0..5, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_ub(4).unwrap();
     let res = solver.solve_assumps(&assumps).unwrap();
     assert_eq!(res, SolverResult::Sat);
 
     enc.extend(vec![lit![6], lit![7], lit![8], lit![9], lit![10]]);
 
-    enc.encode_ub_change(0..5, &mut solver, &mut var_manager);
+    enc.encode_ub_change(0..5, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_ub(4).unwrap();
     let res = solver.solve_assumps(&assumps).unwrap();
     assert_eq!(res, SolverResult::Unsat);
 
-    enc.encode_ub_change(0..8, &mut solver, &mut var_manager);
+    enc.encode_ub_change(0..8, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_ub(7).unwrap();
     let res = solver.solve_assumps(&assumps).unwrap();
     assert_eq!(res, SolverResult::Sat);
@@ -156,7 +167,8 @@ fn test_both_card<CE: BoundBoth + From<Vec<Lit>>>() {
     // Set up totalizer
     let mut enc = CE::from(vec![!lit![0], !lit![1], !lit![2], !lit![3], !lit![4]]);
 
-    enc.encode_both(2..4, &mut solver, &mut var_manager);
+    enc.encode_both(2..4, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_ub(2).unwrap();
     let res = solver.solve_assumps(&assumps).unwrap();
     assert_eq!(res, SolverResult::Sat);
@@ -179,7 +191,8 @@ fn test_both_card_min_enc<CE: BoundBoth + From<Vec<Lit>>>() {
 
     let mut enc = CE::from(vec![lit![0], lit![1], lit![2], lit![3]]);
 
-    enc.encode_both(3..4, &mut solver, &mut var_manager);
+    enc.encode_both(3..4, &mut solver, &mut var_manager)
+        .unwrap();
     let mut assumps = enc.enforce_eq(3).unwrap();
     assumps.extend(vec![lit![0], lit![1], lit![2], !lit![3]]);
     let res = solver.solve_assumps(&assumps).unwrap();
@@ -274,7 +287,7 @@ fn test_ub_exhaustive<CE: BoundUpperIncremental + From<Vec<Lit>>>() {
     let mut var_manager = BasicVarManager::default();
     var_manager.increase_next_free(var![4]);
 
-    enc.encode_ub(0..1, &mut solver, &mut var_manager);
+    enc.encode_ub(0..1, &mut solver, &mut var_manager).unwrap();
     let assumps = enc.enforce_ub(0).unwrap();
 
     test_all!(
@@ -297,7 +310,8 @@ fn test_ub_exhaustive<CE: BoundUpperIncremental + From<Vec<Lit>>>() {
         Sat      // 0000
     );
 
-    enc.encode_ub_change(1..2, &mut solver, &mut var_manager);
+    enc.encode_ub_change(1..2, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_ub(1).unwrap();
 
     test_all!(
@@ -320,7 +334,8 @@ fn test_ub_exhaustive<CE: BoundUpperIncremental + From<Vec<Lit>>>() {
         Sat      // 0000
     );
 
-    enc.encode_ub_change(2..3, &mut solver, &mut var_manager);
+    enc.encode_ub_change(2..3, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_ub(2).unwrap();
 
     test_all!(
@@ -343,7 +358,8 @@ fn test_ub_exhaustive<CE: BoundUpperIncremental + From<Vec<Lit>>>() {
         Sat      // 0000
     );
 
-    enc.encode_ub_change(3..4, &mut solver, &mut var_manager);
+    enc.encode_ub_change(3..4, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_ub(3).unwrap();
 
     test_all!(
@@ -366,7 +382,8 @@ fn test_ub_exhaustive<CE: BoundUpperIncremental + From<Vec<Lit>>>() {
         Sat      // 0000
     );
 
-    enc.encode_ub_change(4..5, &mut solver, &mut var_manager);
+    enc.encode_ub_change(4..5, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_ub(4).unwrap();
 
     test_all!(
@@ -396,7 +413,8 @@ fn test_both_exhaustive<CE: BoundBothIncremental + From<Vec<Lit>>>() {
     let mut var_manager = BasicVarManager::default();
     var_manager.increase_next_free(var![4]);
 
-    enc.encode_both(0..1, &mut solver, &mut var_manager);
+    enc.encode_both(0..1, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_eq(0).unwrap();
 
     test_all!(
@@ -419,7 +437,8 @@ fn test_both_exhaustive<CE: BoundBothIncremental + From<Vec<Lit>>>() {
         Sat      // 0000
     );
 
-    enc.encode_both_change(1..2, &mut solver, &mut var_manager);
+    enc.encode_both_change(1..2, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_eq(1).unwrap();
 
     test_all!(
@@ -442,7 +461,8 @@ fn test_both_exhaustive<CE: BoundBothIncremental + From<Vec<Lit>>>() {
         Unsat    // 0000
     );
 
-    enc.encode_both_change(2..3, &mut solver, &mut var_manager);
+    enc.encode_both_change(2..3, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_eq(2).unwrap();
 
     test_all!(
@@ -465,7 +485,8 @@ fn test_both_exhaustive<CE: BoundBothIncremental + From<Vec<Lit>>>() {
         Unsat    // 0000
     );
 
-    enc.encode_both_change(3..4, &mut solver, &mut var_manager);
+    enc.encode_both_change(3..4, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_eq(3).unwrap();
 
     test_all!(
@@ -488,7 +509,8 @@ fn test_both_exhaustive<CE: BoundBothIncremental + From<Vec<Lit>>>() {
         Unsat    // 0000
     );
 
-    enc.encode_both_change(4..5, &mut solver, &mut var_manager);
+    enc.encode_both_change(4..5, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_eq(4).unwrap();
 
     test_all!(
diff --git a/rustsat/tests/pb_encodings.rs b/rustsat/tests/pb_encodings.rs
index 45dc8b80..176611bf 100644
--- a/rustsat/tests/pb_encodings.rs
+++ b/rustsat/tests/pb_encodings.rs
@@ -49,17 +49,19 @@ fn test_inc_pb_ub<PBE: BoundUpperIncremental + Extend<(Lit, usize)> + Default>()
     let mut enc = PBE::default();
     enc.extend(lits);
 
-    enc.encode_ub(0..3, &mut solver, &mut var_manager);
+    enc.encode_ub(0..3, &mut solver, &mut var_manager).unwrap();
     let assumps = enc.enforce_ub(2).unwrap();
     let res = solver.solve_assumps(&assumps).unwrap();
     assert_eq!(res, SolverResult::Unsat);
 
-    enc.encode_ub_change(0..5, &mut solver, &mut var_manager);
+    enc.encode_ub_change(0..5, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_ub(4).unwrap();
     let res = solver.solve_assumps(&assumps).unwrap();
     assert_eq!(res, SolverResult::Unsat);
 
-    enc.encode_ub_change(0..6, &mut solver, &mut var_manager);
+    enc.encode_ub_change(0..6, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_ub(5).unwrap();
     let res = solver.solve_assumps(&assumps).unwrap();
     assert_eq!(res, SolverResult::Sat);
@@ -68,12 +70,14 @@ fn test_inc_pb_ub<PBE: BoundUpperIncremental + Extend<(Lit, usize)> + Default>()
     lits.insert(lit![5], 4);
     enc.extend(lits);
 
-    enc.encode_ub_change(0..6, &mut solver, &mut var_manager);
+    enc.encode_ub_change(0..6, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_ub(5).unwrap();
     let res = solver.solve_assumps(&assumps).unwrap();
     assert_eq!(res, SolverResult::Unsat);
 
-    enc.encode_ub_change(0..10, &mut solver, &mut var_manager);
+    enc.encode_ub_change(0..10, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_ub(9).unwrap();
     let res = solver.solve_assumps(&assumps).unwrap();
     assert_eq!(res, SolverResult::Sat);
@@ -86,12 +90,14 @@ fn test_inc_pb_ub<PBE: BoundUpperIncremental + Extend<(Lit, usize)> + Default>()
     lits.insert(lit![10], 2);
     enc.extend(lits);
 
-    enc.encode_ub_change(0..10, &mut solver, &mut var_manager);
+    enc.encode_ub_change(0..10, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_ub(9).unwrap();
     let res = solver.solve_assumps(&assumps).unwrap();
     assert_eq!(res, SolverResult::Unsat);
 
-    enc.encode_ub_change(0..15, &mut solver, &mut var_manager);
+    enc.encode_ub_change(0..15, &mut solver, &mut var_manager)
+        .unwrap();
     let assumps = enc.enforce_ub(14).unwrap();
     let res = solver.solve_assumps(&assumps).unwrap();
     assert_eq!(res, SolverResult::Sat);
@@ -109,7 +115,8 @@ fn test_pb_eq<PBE: BoundBothIncremental + From<RsHashMap<Lit, usize>>>() {
     lits.insert(lit![2], 2);
     let mut enc = PBE::from(lits);
 
-    enc.encode_both(4..5, &mut solver, &mut var_manager);
+    enc.encode_both(4..5, &mut solver, &mut var_manager)
+        .unwrap();
 
     let mut assumps = enc.enforce_eq(4).unwrap();
     assumps.extend(vec![lit![0], lit![1], lit![2]]);
@@ -170,7 +177,7 @@ fn test_pb_lb<PBE: BoundLower + From<RsHashMap<Lit, usize>>>() {
     lits.insert(lit![2], 3);
     let mut enc = PBE::from(lits);
 
-    enc.encode_lb(0..11, &mut solver, &mut var_manager);
+    enc.encode_lb(0..11, &mut solver, &mut var_manager).unwrap();
     let assumps = enc.enforce_lb(10).unwrap();
     let res = solver.solve_assumps(&assumps).unwrap();
     assert_eq!(res, SolverResult::Unsat);
@@ -193,7 +200,7 @@ fn test_pb_ub_min_enc<PBE: BoundUpper + From<RsHashMap<Lit, usize>>>() {
     lits.insert(lit![2], 1);
     let mut enc = PBE::from(lits);
 
-    enc.encode_ub(2..3, &mut solver, &mut var_manager);
+    enc.encode_ub(2..3, &mut solver, &mut var_manager).unwrap();
     let mut assumps = enc.enforce_ub(2).unwrap();
     assumps.extend(vec![lit![0], lit![1], lit![2]]);
     let res = solver.solve_assumps(&assumps).unwrap();
@@ -291,7 +298,7 @@ fn test_ub_exhaustive<PBE: BoundUpperIncremental + From<RsHashMap<Lit, usize>>>(
     let mut var_manager = BasicVarManager::default();
     var_manager.increase_next_free(var![4]);
 
-    let max_val = weights.iter().fold(0, |sum, &w| sum + w);
+    let max_val = weights.iter().sum::<usize>();
     let expected = |assign: usize, bound: usize| {
         let sum = (0..4).fold(0, |sum, idx| sum + ((assign >> idx) & 1) * weights[3 - idx]);
         if sum <= bound {
@@ -306,7 +313,8 @@ fn test_ub_exhaustive<PBE: BoundUpperIncremental + From<RsHashMap<Lit, usize>>>(
             bound = max_val - bound;
         }
 
-        enc.encode_ub_change(bound..bound + 1, &mut solver, &mut var_manager);
+        enc.encode_ub_change(bound..bound + 1, &mut solver, &mut var_manager)
+            .unwrap();
         let assumps = enc.enforce_ub(bound).unwrap();
 
         test_all!(