Repository: chrjabs/rustsat (language: python)

Issue:
simp::Glucose bug with solve_assumps
I think the solve simp::Glucose has a bug, where if you keep calling `solve_assumps`, after a few calls it starts producing rubbish.

Unfortunately this doesn't seem to show up with very tiny instances (I guess it needs to be big enough that Glucose does some "interesting simplifications"?)

I attach a little rust project which shows the problem. Basically I load a dimacs file, and try solving with two lists of assumptions -- the first gives a solution, the second fails.

Then I do a bunch of other assumption searches.

Finally, I redo the first 2 tests I did. Now, they both pass, giving the same answer. That second answer is definately wrong, as it doesn't assign variable 3=false (which is part of the assumption).

The code is fixed if I switch simp::Glucose to core::Glucose.




Discussion / hints:

Fix patch:
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index 510ea243..54c50aad 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -24,4 +24,4 @@ jobs:
       - name: Check READMEs
         run: |
           cargo install cargo-rdme
-          for dir in rustsat tools cadical kissat minisat glucose; do cd ${dir} && cargo rdme --check; cd ..; done
\ No newline at end of file
+          for dir in rustsat tools cadical kissat minisat glucose ipasir; do cd ${dir} && (cargo rdme --check || echo "failed for ${dir}"); cd ..; done
diff --git a/.github/workflows/ipasir.yml b/.github/workflows/ipasir.yml
new file mode 100644
index 00000000..e7b1d3c0
--- /dev/null
+++ b/.github/workflows/ipasir.yml
@@ -0,0 +1,30 @@
+name: IPASIR
+
+on:
+  push:
+    branches: [ "main" ]
+  pull_request:
+    branches: [ "main" ]
+
+env:
+  CARGO_TERM_COLOR: always
+    
+jobs:
+  build-test:
+    name: Build
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-latest, windows-latest]
+    runs-on: ${{ matrix.os }}
+    steps:
+      - name: Checkout sources
+        uses: actions/checkout@v4
+      - name: Install stable toolchain
+        uses: dtolnay/rust-toolchain@stable
+      - uses: Swatinem/rust-cache@v2
+        with:
+          shared-key: "build-test"
+      - name: Cargo build
+        run: cargo build -p rustsat-ipasir --verbose
+        env:
+          CMAKE_BUILD_PARALLEL_LEVEL: ${{ fromJSON('["", "4"]')[matrix.os == 'macos-latest'] }}
diff --git a/Cargo.toml b/Cargo.toml
index ed7d733c..cc31a465 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -5,7 +5,8 @@ members = [
   "cadical",
   "kissat",
   "glucose",
-  "minisat"
+  "minisat",
+  "ipasir",
 ]
 resolver = "2"
 
diff --git a/README.md b/README.md
index 01d9a7e1..5408f9b1 100644
--- a/README.md
+++ b/README.md
@@ -40,6 +40,7 @@ These are the crates the project consists of:
 | `rustsat` | The main library, containing basic types, traits, encodings, parsers, and more. |
 | `rustsat-tools` | A collection of small helpful tools based on RustSAT that can be installed as binaries. For a list of available tools, see [this directory](https://github.com/chrjabs/rustsat/tree/main/tools/src/bin) with short descriptions of the tools in the headers of the files. |
 | `rustsat-<satsolver>` | Interfaces to SAT solvers that can be used alongside `rustsat`. Currently interfaces are available for `cadical`, `kissat`, `glucose`, and `minisat`. |
+| `rustsat-ipasir` | [IPASIR](https://github.com/biotomas/ipasir) bindings to use any compliant solver with `rustsat`. |
 
 ## Installation
 
@@ -55,7 +56,6 @@ To install the binary tools in `rustsat-tools` run `cargo install rustsat-tools`
 | --- | --- |
 | `internals` | Make some internal data structures for e.g. encodings public. This is useful when basing a more complex encoding on the `rustsat` implementation of another encoding. Note that the internal API might change between releases. |
 | `fxhash` | Use the faster firefox hash function from `rustc-hash` in `rustsat`. |
-| `ipasir` | Include and link the IPASIR solver interface. |
 | `optimization` | Include optimization (MaxSAT) data structures etc. |
 | `multiopt` | Include data structures etc. for multi-objective optimization. |
 | `compression` | Enable parsing and writing compressed input. |
diff --git a/cadical/Cargo.toml b/cadical/Cargo.toml
index c47e0330..8079e9e9 100644
--- a/cadical/Cargo.toml
+++ b/cadical/Cargo.toml
@@ -37,10 +37,13 @@ v1-9-1 = []
 v1-9-2 = []
 v1-9-3 = []
 v1-9-4 = []
+v1-9-5 = []
 
 [dependencies]
 cpu-time = "1.0.0"
 rustsat = { version = "0.4.3", path = "../rustsat", default-features = false }
+thiserror = { version = "1.0.57" }
+anyhow = { version = "1.0.80" }
 
 [build-dependencies]
 cc = { version = "1.0.83", features = ["parallel"] }
diff --git a/cadical/build-all.sh b/cadical/build-all.sh
index af87bb5c..133f2c83 100755
--- a/cadical/build-all.sh
+++ b/cadical/build-all.sh
@@ -105,6 +105,11 @@ if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo build --features=v1-9-4 &> v194-build.log
 echo "v1.9.4 build returned: $?"
 
+echo "Building v1.9.5"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
+cargo build --features=v1-9-5 &> v195-build.log
+echo "v1.9.5 build returned: $?"
+
 echo "Building quiet"
 if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo build --features=quiet &> quiet-build.log
diff --git a/cadical/build.rs b/cadical/build.rs
index 07384432..bbbe2311 100644
--- a/cadical/build.rs
+++ b/cadical/build.rs
@@ -19,7 +19,9 @@ fn main() {
     compile_error!("cannot combine cadical features quiet and logging");
 
     // Select commit based on features. If conflict, always choose newest release
-    let (tag, patch) = if cfg!(feature = "v1-9-4") {
+    let (tag, patch) = if cfg!(feature = "v1-9-5") {
+        ("refs/tags/rel-1.9.5", "patches/v192.patch")
+    } else if cfg!(feature = "v1-9-4") {
         ("refs/tags/rel-1.9.4", "patches/v192.patch")
     } else if cfg!(feature = "v1-9-3") {
         ("refs/tags/rel-1.9.3", "patches/v192.patch")
@@ -61,7 +63,7 @@ fn main() {
         ("refs/tags/rel-1.5.0", "patches/v150.patch")
     } else {
         // default to newest version
-        ("refs/tags/rel-1.9.4", "patches/v192.patch")
+        ("refs/tags/rel-1.9.5", "patches/v192.patch")
     };
 
     // Build C++ library
@@ -94,8 +96,8 @@ fn build(repo: &str, branch: &str, reference: &str, patch: &str) {
             .filter_map(|res| {
                 if let Ok(p) = res {
                     if let Some(name) = p.file_name() {
-                        if name == "cadical.cpp" || name == "mobical.cpp" {
-                            return None; // Filter out application files
+                        if name == "cadical.cpp" || name == "mobical.cpp" || name == "ipasir.cpp" {
+                            return None; // Filter out application files and IPASIR interface
                         }
                     };
                     Some(p)
diff --git a/cadical/src/lib.rs b/cadical/src/lib.rs
index 65c18db8..c9ef6d13 100644
--- a/cadical/src/lib.rs
+++ b/cadical/src/lib.rs
@@ -27,10 +27,18 @@ use cpu_time::ProcessTime;
 use ffi::CaDiCaLHandle;
 use rustsat::solvers::{
     ControlSignal, FreezeVar, GetInternalStats, Interrupt, InterruptSolver, Learn, LimitConflicts,
-    LimitDecisions, PhaseLit, Solve, SolveIncremental, SolveMightFail, SolveStats, SolverError,
-    SolverResult, SolverState, SolverStats, Terminate,
+    LimitDecisions, PhaseLit, Solve, SolveIncremental, SolveStats, SolverResult, SolverState,
+    SolverStats, StateError, Terminate,
 };
 use rustsat::types::{Clause, Lit, TernaryVal, Var};
+use thiserror::Error;
+
+#[derive(Error, Clone, Copy, PartialEq, Eq, Debug)]
+#[error("cadical c-api returned an invalid value: {api_call} -> {value}")]
+pub struct InvalidApiReturn {
+    api_call: &'static str,
+    value: c_int,
+}
 
 #[derive(Debug, PartialEq, Eq, Default)]
 enum InternalSolverState {
@@ -84,17 +92,17 @@ impl Default for CaDiCaL<'_, '_> {
 }
 
 impl CaDiCaL<'_, '_> {
-    fn get_core_assumps(&self, assumps: &[Lit]) -> Result<Vec<Lit>, SolverError> {
+    fn get_core_assumps(&self, assumps: &[Lit]) -> Result<Vec<Lit>, InvalidApiReturn> {
         let mut core = Vec::new();
         for a in assumps {
             match unsafe { ffi::ccadical_failed(self.handle, a.to_ipasir()) } {
                 0 => (),
                 1 => core.push(!*a),
-                invalid => {
-                    return Err(SolverError::Api(format!(
-                        "ccadical_failed returned invalid value: {}",
-                        invalid
-                    )))
+                value => {
+                    return Err(InvalidApiReturn {
+                        api_call: "ccadical_failed",
+                        value,
+                    })
                 }
             }
         }
@@ -124,17 +132,21 @@ impl CaDiCaL<'_, '_> {
     /// Checks whether the temporary clause is part of the core if in
     /// unsatisfiable state. This needs to always be checked in addition to
     /// [`SolveIncremental::core`] if a [`CaDiCaL::add_tmp_clause`] is used.
-    pub fn tmp_clause_in_core(&mut self) -> Result<bool, SolverError> {
+    pub fn tmp_clause_in_core(&mut self) -> anyhow::Result<bool> {
         match &self.state {
             InternalSolverState::Unsat(_) => unsafe {
                 Ok(ffi::ccadical_constraint_failed(self.handle) != 0)
             },
-            state => Err(SolverError::State(state.to_external(), SolverState::Unsat)),
+            state => Err(StateError {
+                required_state: SolverState::Unsat,
+                actual_state: state.to_external(),
+            }
+            .into()),
         }
     }
 
     /// Sets a pre-defined configuration for CaDiCaL's internal options
-    pub fn set_configuration(&mut self, config: Config) -> SolveMightFail {
+    pub fn set_configuration(&mut self, config: Config) -> anyhow::Result<()> {
         if self.state == InternalSolverState::Configuring {
             let config_name = match config {
                 Config::Default => CString::new("default").unwrap(),
@@ -146,15 +158,18 @@ impl CaDiCaL<'_, '_> {
             if ret {
                 Ok(())
             } else {
-                Err(SolverError::Api(
-                    "ccadical_configure returned false".to_string(),
-                ))
+                Err(InvalidApiReturn {
+                    api_call: "ccadical_configure",
+                    value: 0,
+                }
+                .into())
             }
         } else {
-            Err(SolverError::State(
-                self.state.to_external(),
-                SolverState::Configuring,
-            ))
+            Err(StateError {
+                required_state: SolverState::Configuring,
+                actual_state: self.state.to_external(),
+            }
+            .into())
         }
     }
 
@@ -167,23 +182,16 @@ impl CaDiCaL<'_, '_> {
     /// and `<val>` can be parsed then 'true' is returned.  If the option value
     /// is out of range the actual value is computed as the closest (minimum or
     /// maximum) value possible, but still `true` is returned.
-    pub fn set_option(&mut self, name: &str, value: c_int) -> SolveMightFail {
-        let c_name = match CString::new(name) {
-            Ok(cstr) => cstr,
-            Err(_) => {
-                return Err(SolverError::Api(format!(
-                    "CaDiCaL option {} cannot be converted to a C string",
-                    name
-                )))
-            }
-        };
+    pub fn set_option(&mut self, name: &str, value: c_int) -> anyhow::Result<()> {
+        let c_name = CString::new(name)?;
         if unsafe { ffi::ccadical_set_option_ret(self.handle, c_name.as_ptr(), value) } {
             Ok(())
         } else {
-            Err(SolverError::Api(format!(
-                "ccadical_set_option_ret returned false for option {}",
-                name
-            )))
+            Err(InvalidApiReturn {
+                api_call: "ccadical_set_option_ret",
+                value: 0,
+            }
+            .into())
         }
     }
 
@@ -193,16 +201,8 @@ impl CaDiCaL<'_, '_> {
     ///
     /// Get the current value of the option `name`.  If `name` is invalid then
     /// zero is returned.
-    pub fn get_option(&self, name: &str) -> Result<c_int, SolverError> {
-        let c_name = match CString::new(name) {
-            Ok(cstr) => cstr,
-            Err(_) => {
-                return Err(SolverError::Api(format!(
-                    "CaDiCaL option {} cannot be converted to a C string",
-                    name
-                )))
-            }
-        };
+    pub fn get_option(&self, name: &str) -> anyhow::Result<c_int> {
+        let c_name = CString::new(name)?;
         Ok(unsafe { ffi::ccadical_get_option(self.handle, c_name.as_ptr()) })
     }
 
@@ -223,7 +223,7 @@ impl CaDiCaL<'_, '_> {
     /// well as overwritten and reset during calls to `simplify` and
     /// `lookahead`).  We actually also have an internal "terminate" limit
     /// which however should only be used for testing and debugging.
-    pub fn set_limit(&mut self, limit: Limit) -> SolveMightFail {
+    pub fn set_limit(&mut self, limit: Limit) -> anyhow::Result<()> {
         let (name, val) = match limit {
             Limit::Terminate(val) => (CString::new("terminate").unwrap(), val),
             Limit::Conflicts(val) => (CString::new("conflicts").unwrap(), val),
@@ -234,10 +234,11 @@ impl CaDiCaL<'_, '_> {
         if unsafe { ffi::ccadical_limit_ret(self.handle, name.as_ptr(), val) } {
             Ok(())
         } else {
-            Err(SolverError::Api(format!(
-                "ccadical_limit_ret returned false for limit {}",
-                limit
-            )))
+            Err(InvalidApiReturn {
+                api_call: "ccadical_limit_ret",
+                value: 0,
+            }
+            .into())
         }
     }
 
@@ -271,22 +272,15 @@ impl CaDiCaL<'_, '_> {
         unsafe { ffi::ccadical_print_statistics(self.handle) }
     }
 
-    pub fn simplify(&mut self, rounds: u32) -> Result<SolverResult, SolverError> {
+    pub fn simplify(&mut self, rounds: u32) -> anyhow::Result<SolverResult> {
         // If already solved, return state
         if let InternalSolverState::Sat = self.state {
             return Ok(SolverResult::Sat);
-        } else if let InternalSolverState::Unsat(_) = self.state {
+        }
+        if let InternalSolverState::Unsat(_) = self.state {
             return Ok(SolverResult::Unsat);
         }
-        let rounds: c_int = match rounds.try_into() {
-            Ok(val) => val,
-            Err(_) => {
-                return Err(SolverError::Api(format!(
-                    "rounds value {} does not fit into c_int",
-                    rounds
-                )))
-            }
-        };
+        let rounds: c_int = rounds.try_into()?;
         // Simplify with CaDiCaL backend
         match unsafe { ffi::ccadical_simplify_rounds(self.handle, rounds) } {
             0 => {
@@ -301,10 +295,11 @@ impl CaDiCaL<'_, '_> {
                 self.state = InternalSolverState::Unsat(vec![]);
                 Ok(SolverResult::Unsat)
             }
-            invalid => Err(SolverError::Api(format!(
-                "ccadical_simplify returned invalid value: {}",
-                invalid
-            ))),
+            value => Err(InvalidApiReturn {
+                api_call: "ccadical_simplify",
+                value,
+            }
+            .into()),
         }
     }
 
@@ -312,22 +307,15 @@ impl CaDiCaL<'_, '_> {
         &mut self,
         assumps: Vec<Lit>,
         rounds: u32,
-    ) -> Result<SolverResult, SolverError> {
+    ) -> anyhow::Result<SolverResult> {
         // If already solved, return state
         if let InternalSolverState::Sat = self.state {
             return Ok(SolverResult::Sat);
-        } else if let InternalSolverState::Unsat(_) = self.state {
+        }
+        if let InternalSolverState::Unsat(_) = self.state {
             return Ok(SolverResult::Unsat);
         }
-        let rounds: c_int = match rounds.try_into() {
-            Ok(val) => val,
-            Err(_) => {
-                return Err(SolverError::Api(format!(
-                    "rounds value {} does not fit into c_int",
-                    rounds
-                )))
-            }
-        };
+        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()) }
@@ -345,10 +333,11 @@ impl CaDiCaL<'_, '_> {
                 self.state = InternalSolverState::Unsat(vec![]);
                 Ok(SolverResult::Unsat)
             }
-            invalid => Err(SolverError::Api(format!(
-                "ccadical_simplify returned invalid value: {}",
-                invalid
-            ))),
+            value => Err(InvalidApiReturn {
+                api_call: "ccadical_simplify",
+                value,
+            }
+            .into()),
         }
     }
 }
@@ -369,17 +358,18 @@ impl Solve for CaDiCaL<'_, '_> {
             .expect("CaDiCaL signature returned invalid UTF-8.")
     }
 
-    fn reserve(&mut self, max_var: Var) -> SolveMightFail {
+    fn reserve(&mut self, max_var: Var) -> anyhow::Result<()> {
         self.state = InternalSolverState::Input;
         unsafe { ffi::ccadical_reserve(self.handle, max_var.to_ipasir()) };
         Ok(())
     }
 
-    fn solve(&mut self) -> Result<SolverResult, SolverError> {
+    fn solve(&mut self) -> anyhow::Result<SolverResult> {
         // If already solved, return state
         if let InternalSolverState::Sat = self.state {
             return Ok(SolverResult::Sat);
-        } else if let InternalSolverState::Unsat(core) = &self.state {
+        }
+        if let InternalSolverState::Unsat(core) = &self.state {
             if core.is_empty() {
                 return Ok(SolverResult::Unsat);
             }
@@ -404,34 +394,38 @@ impl Solve for CaDiCaL<'_, '_> {
                 self.state = InternalSolverState::Unsat(vec![]);
                 Ok(SolverResult::Unsat)
             }
-            invalid => Err(SolverError::Api(format!(
-                "ccadical_solve returned invalid value: {}",
-                invalid
-            ))),
+            value => Err(InvalidApiReturn {
+                api_call: "ccadical_solve",
+                value,
+            }
+            .into()),
         }
     }
 
-    fn lit_val(&self, lit: Lit) -> Result<TernaryVal, SolverError> {
-        match &self.state {
-            InternalSolverState::Sat => {
-                let lit = lit.to_ipasir();
-                match unsafe { ffi::ccadical_val(self.handle, lit) } {
-                    0 => Ok(TernaryVal::DontCare),
-                    p if p == lit => Ok(TernaryVal::True),
-                    n if n == -lit => Ok(TernaryVal::False),
-                    // CaDiCaL returns -1 if variable is higher than max var
-                    dc if dc == -1 => Ok(TernaryVal::DontCare),
-                    invalid => Err(SolverError::Api(format!(
-                        "ccadical_val returned invalid value: {}",
-                        invalid
-                    ))),
-                }
+    fn lit_val(&self, lit: Lit) -> anyhow::Result<TernaryVal> {
+        if self.state != InternalSolverState::Sat {
+            return Err(StateError {
+                required_state: SolverState::Sat,
+                actual_state: self.state.to_external(),
+            }
+            .into());
+        }
+        let lit = lit.to_ipasir();
+        match unsafe { ffi::ccadical_val(self.handle, lit) } {
+            0 => Ok(TernaryVal::DontCare),
+            p if p == lit => Ok(TernaryVal::True),
+            n if n == -lit => Ok(TernaryVal::False),
+            // CaDiCaL returns -1 if variable is higher than max var
+            dc if dc == -1 => Ok(TernaryVal::DontCare),
+            value => Err(InvalidApiReturn {
+                api_call: "ccadical_val",
+                value,
             }
-            other => Err(SolverError::State(other.to_external(), SolverState::Sat)),
+            .into()),
         }
     }
 
-    fn add_clause(&mut self, clause: Clause) -> SolveMightFail {
+    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> {
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         self.stats.avg_clause_len =
@@ -448,7 +442,7 @@ impl Solve for CaDiCaL<'_, '_> {
 }
 
 impl SolveIncremental for CaDiCaL<'_, '_> {
-    fn solve_assumps(&mut self, assumps: &[Lit]) -> Result<SolverResult, SolverError> {
+    fn solve_assumps(&mut self, assumps: &[Lit]) -> anyhow::Result<SolverResult> {
         let start = ProcessTime::now();
         // Solve with CaDiCaL backend
         for a in assumps {
@@ -472,17 +466,22 @@ impl SolveIncremental for CaDiCaL<'_, '_> {
                 self.state = InternalSolverState::Unsat(self.get_core_assumps(assumps)?);
                 Ok(SolverResult::Unsat)
             }
-            invalid => Err(SolverError::Api(format!(
-                "ccadical_solve returned invalid value: {}",
-                invalid
-            ))),
+            value => Err(InvalidApiReturn {
+                api_call: "ccadical_solve",
+                value,
+            }
+            .into()),
         }
     }
 
-    fn core(&mut self) -> Result<Vec<Lit>, SolverError> {
+    fn core(&mut self) -> anyhow::Result<Vec<Lit>> {
         match &self.state {
             InternalSolverState::Unsat(core) => Ok(core.clone()),
-            other => Err(SolverError::State(other.to_external(), SolverState::Unsat)),
+            other => Err(StateError {
+                required_state: SolverState::Unsat,
+                actual_state: other.to_external(),
+            }
+            .into()),
         }
     }
 }
@@ -608,31 +607,31 @@ impl InterruptSolver for Interrupter {
 
 impl PhaseLit for CaDiCaL<'_, '_> {
     /// Forces the default decision phase of a variable to a certain value
-    fn phase_lit(&mut self, lit: Lit) -> Result<(), SolverError> {
+    fn phase_lit(&mut self, lit: Lit) -> anyhow::Result<()> {
         unsafe { ffi::ccadical_phase(self.handle, lit.to_ipasir()) };
         Ok(())
     }
 
     /// Undoes the effect of a call to [`CaDiCaL::phase_lit`]
-    fn unphase_var(&mut self, var: Var) -> Result<(), SolverError> {
+    fn unphase_var(&mut self, var: Var) -> anyhow::Result<()> {
         unsafe { ffi::ccadical_unphase(self.handle, var.to_ipasir()) };
         Ok(())
     }
 }
 
 impl FreezeVar for CaDiCaL<'_, '_> {
-    fn freeze_var(&mut self, var: Var) -> Result<(), SolverError> {
-        unsafe { ffi::ccadical_freeze(self.handle, var.pos_lit().to_ipasir()) };
+    fn freeze_var(&mut self, var: Var) -> anyhow::Result<()> {
+        unsafe { ffi::ccadical_freeze(self.handle, var.to_ipasir()) };
         Ok(())
     }
 
-    fn melt_var(&mut self, var: Var) -> Result<(), SolverError> {
-        unsafe { ffi::ccadical_melt(self.handle, var.pos_lit().to_ipasir()) };
+    fn melt_var(&mut self, var: Var) -> anyhow::Result<()> {
+        unsafe { ffi::ccadical_melt(self.handle, var.to_ipasir()) };
         Ok(())
     }
 
-    fn is_frozen(&mut self, var: Var) -> Result<bool, SolverError> {
-        Ok(unsafe { ffi::ccadical_frozen(self.handle, var.pos_lit().to_ipasir()) } != 0)
+    fn is_frozen(&mut self, var: Var) -> anyhow::Result<bool> {
+        Ok(unsafe { ffi::ccadical_frozen(self.handle, var.to_ipasir()) } != 0)
     }
 }
 
@@ -651,29 +650,31 @@ impl FreezeVar for CaDiCaL<'_, '_> {
     )
 ))]
 impl rustsat::solvers::FlipLit for CaDiCaL<'_, '_> {
-    fn flip_lit(&mut self, lit: Lit) -> Result<bool, SolverError> {
+    fn flip_lit(&mut self, lit: Lit) -> anyhow::Result<bool> {
         if self.state != InternalSolverState::Sat {
-            return Err(SolverError::State(
-                self.state.to_external(),
-                SolverState::Sat,
-            ));
+            return Err(StateError {
+                required_state: SolverState::Sat,
+                actual_state: self.state.to_external(),
+            }
+            .into());
         }
         Ok(unsafe { ffi::ccadical_flip(self.handle, lit.to_ipasir()) })
     }
 
-    fn is_flippable(&mut self, lit: Lit) -> Result<bool, SolverError> {
+    fn is_flippable(&mut self, lit: Lit) -> anyhow::Result<bool> {
         if self.state != InternalSolverState::Sat {
-            return Err(SolverError::State(
-                self.state.to_external(),
-                SolverState::Sat,
-            ));
+            return Err(StateError {
+                required_state: SolverState::Sat,
+                actual_state: self.state.to_external(),
+            }
+            .into());
         }
         Ok(unsafe { ffi::ccadical_flippable(self.handle, lit.to_ipasir()) })
     }
 }
 
 impl LimitConflicts for CaDiCaL<'_, '_> {
-    fn limit_conflicts(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
+    fn limit_conflicts(&mut self, limit: Option<u32>) -> anyhow::Result<()> {
         self.set_limit(Limit::Conflicts(if let Some(limit) = limit {
             limit as c_int
         } else {
@@ -683,7 +684,7 @@ impl LimitConflicts for CaDiCaL<'_, '_> {
 }
 
 impl LimitDecisions for CaDiCaL<'_, '_> {
-    fn limit_decisions(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
+    fn limit_decisions(&mut self, limit: Option<u32>) -> anyhow::Result<()> {
         self.set_limit(Limit::Decisions(if let Some(limit) = limit {
             limit as c_int
         } else {
@@ -798,7 +799,7 @@ mod test {
     use rustsat::{
         lit,
         solvers::{
-            ControlSignal, FreezeVar, Learn, Solve, SolverError, SolverResult, SolverState,
+            ControlSignal, FreezeVar, Learn, Solve, SolverResult, SolverState, StateError,
             Terminate,
         },
         types::TernaryVal,
@@ -885,7 +886,6 @@ mod test {
         solver.add_unit(!lit![0]).unwrap();
 
         let mut cl_len = 0;
-        let ret;
 
         solver.attach_learner(
             |clause| {
@@ -894,7 +894,7 @@ mod test {
             10,
         );
 
-        ret = solver.solve();
+        let ret = solver.solve();
 
         drop(solver);
 
@@ -916,13 +916,13 @@ mod test {
         solver.set_configuration(Config::SAT).unwrap();
         solver.set_configuration(Config::UNSAT).unwrap();
         solver.add_unit(lit![0]).unwrap();
-        assert_eq!(
-            solver.set_configuration(Config::Default),
-            Err(SolverError::State(
-                SolverState::Input,
-                SolverState::Configuring
-            ))
-        );
+        assert!(solver.set_configuration(Config::Default).is_err_and(|e| e
+            .downcast::<StateError>()
+            .unwrap()
+            == StateError {
+                required_state: SolverState::Configuring,
+                actual_state: SolverState::Input
+            }));
     }
 
     #[test]
diff --git a/glucose/Cargo.toml b/glucose/Cargo.toml
index 81ba2383..62879b18 100644
--- a/glucose/Cargo.toml
+++ b/glucose/Cargo.toml
@@ -21,6 +21,8 @@ default = ["quiet"]
 [dependencies]
 cpu-time = "1.0.0"
 rustsat = { version = "0.4.3", path = "../rustsat", default-features = false }
+thiserror = { version = "1.0.57" }
+anyhow = { version = "1.0.80" }
 
 [build-dependencies]
 cc = { version = "1.0.83", features = ["parallel"] }
diff --git a/glucose/build.rs b/glucose/build.rs
index 7c184512..d2e37b85 100644
--- a/glucose/build.rs
+++ b/glucose/build.rs
@@ -11,7 +11,7 @@ fn main() {
     build(
         "https://github.com/chrjabs/glucose4.git",
         "main",
-        "2c41a6d2e9c8db7b5bdebc8dc65760d01bc938e9",
+        "a244a12a3f34da6c93377a6196291494fddf491e",
     );
 
     let out_dir = env::var("OUT_DIR").unwrap();
diff --git a/glucose/src/core.rs b/glucose/src/core.rs
index c56fd810..29d78fe8 100644
--- a/glucose/src/core.rs
+++ b/glucose/src/core.rs
@@ -5,14 +5,13 @@
 
 use core::ffi::{c_int, CStr};
 
-use super::{InternalSolverState, Limit};
+use super::{InternalSolverState, InvalidApiReturn, Limit};
 use cpu_time::ProcessTime;
 use ffi::Glucose4Handle;
 use rustsat::{
     solvers::{
         GetInternalStats, Interrupt, InterruptSolver, LimitConflicts, LimitPropagations, PhaseLit,
-        Solve, SolveIncremental, SolveMightFail, SolveStats, SolverError, SolverResult,
-        SolverState, SolverStats,
+        Solve, SolveIncremental, SolveStats, SolverResult, SolverState, SolverStats, StateError,
     },
     types::{Clause, Lit, TernaryVal, Var},
 };
@@ -35,17 +34,17 @@ impl Default for Glucose {
 }
 
 impl Glucose {
-    fn get_core_assumps(&self, assumps: &[Lit]) -> Result<Vec<Lit>, SolverError> {
+    fn get_core_assumps(&self, assumps: &[Lit]) -> Result<Vec<Lit>, InvalidApiReturn> {
         let mut core = Vec::new();
         for a in assumps {
             match unsafe { ffi::cglucose4_failed(self.handle, a.to_ipasir()) } {
                 0 => (),
                 1 => core.push(!*a),
-                invalid => {
-                    return Err(SolverError::Api(format!(
-                        "cglucose4_failed returned invalid value: {}",
-                        invalid
-                    )))
+                value => {
+                    return Err(InvalidApiReturn {
+                        api_call: "cglucose4_failed",
+                        value,
+                    })
                 }
             }
         }
@@ -90,11 +89,12 @@ impl Solve for Glucose {
             .expect("Glucose 4 signature returned invalid UTF-8.")
     }
 
-    fn solve(&mut self) -> Result<SolverResult, SolverError> {
+    fn solve(&mut self) -> anyhow::Result<SolverResult> {
         // If already solved, return state
         if let InternalSolverState::Sat = self.state {
             return Ok(SolverResult::Sat);
-        } else if let InternalSolverState::Unsat(core) = &self.state {
+        }
+        if let InternalSolverState::Unsat(core) = &self.state {
             if core.is_empty() {
                 return Ok(SolverResult::Unsat);
             }
@@ -119,32 +119,36 @@ impl Solve for Glucose {
                 self.state = InternalSolverState::Unsat(vec![]);
                 Ok(SolverResult::Unsat)
             }
-            invalid => Err(SolverError::Api(format!(
-                "cglucose4_solve returned invalid value: {}",
-                invalid
-            ))),
+            value => Err(InvalidApiReturn {
+                api_call: "cglucose4_solve",
+                value,
+            }
+            .into()),
         }
     }
 
-    fn lit_val(&self, lit: Lit) -> Result<TernaryVal, SolverError> {
-        match &self.state {
-            InternalSolverState::Sat => {
-                let lit = lit.to_ipasir();
-                match unsafe { ffi::cglucose4_val(self.handle, lit) } {
-                    0 => Ok(TernaryVal::DontCare),
-                    p if p == lit => Ok(TernaryVal::True),
-                    n if n == -lit => Ok(TernaryVal::False),
-                    invalid => Err(SolverError::Api(format!(
-                        "cglucose4_val returned invalid value: {}",
-                        invalid
-                    ))),
-                }
+    fn lit_val(&self, lit: Lit) -> anyhow::Result<TernaryVal> {
+        if self.state != InternalSolverState::Sat {
+            return Err(StateError {
+                required_state: SolverState::Sat,
+                actual_state: self.state.to_external(),
             }
-            other => Err(SolverError::State(other.to_external(), SolverState::Sat)),
+            .into());
+        }
+        let lit = lit.to_ipasir();
+        match unsafe { ffi::cglucose4_val(self.handle, lit) } {
+            0 => Ok(TernaryVal::DontCare),
+            p if p == lit => Ok(TernaryVal::True),
+            n if n == -lit => Ok(TernaryVal::False),
+            value => Err(InvalidApiReturn {
+                api_call: "cglucose4_val",
+                value,
+            }
+            .into()),
         }
     }
 
-    fn add_clause(&mut self, clause: Clause) -> SolveMightFail {
+    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> {
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         self.stats.avg_clause_len =
@@ -161,7 +165,7 @@ impl Solve for Glucose {
 }
 
 impl SolveIncremental for Glucose {
-    fn solve_assumps(&mut self, assumps: &[Lit]) -> Result<SolverResult, SolverError> {
+    fn solve_assumps(&mut self, assumps: &[Lit]) -> anyhow::Result<SolverResult> {
         let start = ProcessTime::now();
         // Solve with glucose backend
         for a in assumps {
@@ -185,17 +189,22 @@ impl SolveIncremental for Glucose {
                 self.state = InternalSolverState::Unsat(self.get_core_assumps(assumps)?);
                 Ok(SolverResult::Unsat)
             }
-            invalid => Err(SolverError::Api(format!(
-                "cglucose4_solve returned invalid value: {}",
-                invalid
-            ))),
+            value => Err(InvalidApiReturn {
+                api_call: "cglucose4_solve",
+                value,
+            }
+            .into()),
         }
     }
 
-    fn core(&mut self) -> Result<Vec<Lit>, SolverError> {
+    fn core(&mut self) -> anyhow::Result<Vec<Lit>> {
         match &self.state {
             InternalSolverState::Unsat(core) => Ok(core.clone()),
-            other => Err(SolverError::State(other.to_external(), SolverState::Unsat)),
+            other => Err(StateError {
+                required_state: SolverState::Unsat,
+                actual_state: other.to_external(),
+            }
+            .into()),
         }
     }
 }
@@ -226,20 +235,20 @@ 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) -> Result<(), SolverError> {
+    fn phase_lit(&mut self, lit: Lit) -> anyhow::Result<()> {
         unsafe { ffi::cglucose4_phase(self.handle, lit.to_ipasir()) };
         Ok(())
     }
 
     /// Undoes the effect of a call to [`Glucose::phase_lit`]
-    fn unphase_var(&mut self, var: Var) -> Result<(), SolverError> {
+    fn unphase_var(&mut self, var: Var) -> anyhow::Result<()> {
         unsafe { ffi::cglucose4_unphase(self.handle, var.to_ipasir()) };
         Ok(())
     }
 }
 
 impl LimitConflicts for Glucose {
-    fn limit_conflicts(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
+    fn limit_conflicts(&mut self, limit: Option<u32>) -> anyhow::Result<()> {
         self.set_limit(Limit::Conflicts(if let Some(limit) = limit {
             limit as i64
         } else {
@@ -250,7 +259,7 @@ impl LimitConflicts for Glucose {
 }
 
 impl LimitPropagations for Glucose {
-    fn limit_propagations(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
+    fn limit_propagations(&mut self, limit: Option<u32>) -> anyhow::Result<()> {
         self.set_limit(Limit::Propagations(if let Some(limit) = limit {
             limit as i64
         } else {
diff --git a/glucose/src/lib.rs b/glucose/src/lib.rs
index 4f1f0efa..887e0038 100644
--- a/glucose/src/lib.rs
+++ b/glucose/src/lib.rs
@@ -12,12 +12,27 @@
 //! The version of Glucose in this crate is Version 4.2.1.
 //! The used C++ source repository can be found [here](https://github.com/chrjabs/glucose4).
 
-use rustsat::{solvers::SolverState, types::Lit};
-use std::fmt;
+use rustsat::{
+    solvers::SolverState,
+    types::{Lit, Var},
+};
+use std::{ffi::c_int, fmt};
+use thiserror::Error;
 
 pub mod core;
 pub mod simp;
 
+#[derive(Error, Clone, Copy, PartialEq, Eq, Debug)]
+#[error("glucose c-api returned an invalid value: {api_call} -> {value}")]
+pub struct InvalidApiReturn {
+    api_call: &'static str,
+    value: c_int,
+}
+
+#[derive(Error, Clone, Copy, PartialEq, Eq, Debug)]
+#[error("assumption variable {0} has been eliminated by glucose simplification")]
+pub struct AssumpEliminated(Var);
+
 #[derive(Debug, PartialEq, Eq, Default)]
 enum InternalSolverState {
     #[default]
diff --git a/glucose/src/simp.rs b/glucose/src/simp.rs
index 7acce3ad..48dd291c 100644
--- a/glucose/src/simp.rs
+++ b/glucose/src/simp.rs
@@ -5,14 +5,14 @@
 
 use core::ffi::{c_int, CStr};
 
-use super::{InternalSolverState, Limit};
+use super::{AssumpEliminated, InternalSolverState, InvalidApiReturn, Limit};
 use cpu_time::ProcessTime;
 use ffi::Glucose4Handle;
 use rustsat::{
     solvers::{
-        GetInternalStats, Interrupt, InterruptSolver, LimitConflicts, LimitPropagations, PhaseLit,
-        Solve, SolveIncremental, SolveMightFail, SolveStats, SolverError, SolverResult,
-        SolverState, SolverStats,
+        FreezeVar, GetInternalStats, Interrupt, InterruptSolver, LimitConflicts, LimitPropagations,
+        PhaseLit, Solve, SolveIncremental, SolveStats, SolverResult, SolverState, SolverStats,
+        StateError,
     },
     types::{Clause, Lit, TernaryVal, Var},
 };
@@ -35,17 +35,17 @@ impl Default for Glucose {
 }
 
 impl Glucose {
-    fn get_core_assumps(&self, assumps: &[Lit]) -> Result<Vec<Lit>, SolverError> {
+    fn get_core_assumps(&self, assumps: &[Lit]) -> Result<Vec<Lit>, InvalidApiReturn> {
         let mut core = Vec::new();
         for a in assumps {
             match unsafe { ffi::cglucosesimp4_failed(self.handle, a.to_ipasir()) } {
                 0 => (),
                 1 => core.push(!*a),
-                invalid => {
-                    return Err(SolverError::Api(format!(
-                        "cglucosesimp4_failed returned invalid value: {}",
-                        invalid
-                    )))
+                value => {
+                    return Err(InvalidApiReturn {
+                        api_call: "cglucosesimp4_failed",
+                        value,
+                    })
                 }
             }
         }
@@ -75,19 +75,9 @@ impl Glucose {
         unsafe { ffi::cglucosesimp4_n_learnts(self.handle) }
     }
 
-    /// Freezes a literal.
-    pub fn freeze_lit(&mut self, lit: Lit) {
-        unsafe { ffi::cglucosesimp4_set_frozen(self.handle, lit.var().to_ipasir(), true) }
-    }
-
-    /// Melts a literal.
-    pub fn melt_lit(&mut self, lit: Lit) {
-        unsafe { ffi::cglucosesimp4_set_frozen(self.handle, lit.var().to_ipasir(), false) }
-    }
-
     /// Checks if a variable has been eliminated by preprocessing.
-    pub fn var_eliminated(&mut self, var: Var) {
-        unsafe { ffi::cglucosesimp4_is_eliminated(self.handle, var.to_ipasir()) }
+    pub fn var_eliminated(&mut self, var: Var) -> bool {
+        (unsafe { ffi::cglucosesimp4_is_eliminated(self.handle, var.to_ipasir()) } != 0)
     }
 }
 
@@ -107,11 +97,12 @@ impl Solve for Glucose {
             .expect("Glucose 4 signature returned invalid UTF-8.")
     }
 
-    fn solve(&mut self) -> Result<SolverResult, SolverError> {
+    fn solve(&mut self) -> anyhow::Result<SolverResult> {
         // If already solved, return state
         if let InternalSolverState::Sat = self.state {
             return Ok(SolverResult::Sat);
-        } else if let InternalSolverState::Unsat(core) = &self.state {
+        }
+        if let InternalSolverState::Unsat(core) = &self.state {
             if core.is_empty() {
                 return Ok(SolverResult::Unsat);
             }
@@ -136,32 +127,36 @@ impl Solve for Glucose {
                 self.state = InternalSolverState::Unsat(vec![]);
                 Ok(SolverResult::Unsat)
             }
-            invalid => Err(SolverError::Api(format!(
-                "cglucosesimp4_solve returned invalid value: {}",
-                invalid
-            ))),
+            value => Err(InvalidApiReturn {
+                api_call: "cglucosesimp4_solve",
+                value,
+            }
+            .into()),
         }
     }
 
-    fn lit_val(&self, lit: Lit) -> Result<TernaryVal, SolverError> {
-        match &self.state {
-            InternalSolverState::Sat => {
-                let lit = lit.to_ipasir();
-                match unsafe { ffi::cglucosesimp4_val(self.handle, lit) } {
-                    0 => Ok(TernaryVal::DontCare),
-                    p if p == lit => Ok(TernaryVal::True),
-                    n if n == -lit => Ok(TernaryVal::False),
-                    invalid => Err(SolverError::Api(format!(
-                        "cglucosesimp4_val returned invalid value: {}",
-                        invalid
-                    ))),
-                }
+    fn lit_val(&self, lit: Lit) -> anyhow::Result<TernaryVal> {
+        if self.state != InternalSolverState::Sat {
+            return Err(StateError {
+                required_state: SolverState::Sat,
+                actual_state: self.state.to_external(),
+            }
+            .into());
+        }
+        let lit = lit.to_ipasir();
+        match unsafe { ffi::cglucosesimp4_val(self.handle, lit) } {
+            0 => Ok(TernaryVal::DontCare),
+            p if p == lit => Ok(TernaryVal::True),
+            n if n == -lit => Ok(TernaryVal::False),
+            value => Err(InvalidApiReturn {
+                api_call: "cglucosesimp4_val",
+                value,
             }
-            other => Err(SolverError::State(other.to_external(), SolverState::Sat)),
+            .into()),
         }
     }
 
-    fn add_clause(&mut self, clause: Clause) -> SolveMightFail {
+    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> {
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         self.stats.avg_clause_len =
@@ -178,9 +173,14 @@ impl Solve for Glucose {
 }
 
 impl SolveIncremental for Glucose {
-    fn solve_assumps(&mut self, assumps: &[Lit]) -> Result<SolverResult, SolverError> {
+    fn solve_assumps(&mut self, assumps: &[Lit]) -> anyhow::Result<SolverResult> {
         let start = ProcessTime::now();
         // Solve with glucose backend
+        for a in assumps {
+            if self.var_eliminated(a.var()) {
+                return Err(AssumpEliminated(a.var()).into());
+            }
+        }
         for a in assumps {
             unsafe { ffi::cglucosesimp4_assume(self.handle, a.to_ipasir()) }
         }
@@ -202,17 +202,22 @@ impl SolveIncremental for Glucose {
                 self.state = InternalSolverState::Unsat(self.get_core_assumps(assumps)?);
                 Ok(SolverResult::Unsat)
             }
-            invalid => Err(SolverError::Api(format!(
-                "cglucosesimp4_solve returned invalid value: {}",
-                invalid
-            ))),
+            value => Err(InvalidApiReturn {
+                api_call: "cglucosesimp4_solve",
+                value,
+            }
+            .into()),
         }
     }
 
-    fn core(&mut self) -> Result<Vec<Lit>, SolverError> {
+    fn core(&mut self) -> anyhow::Result<Vec<Lit>> {
         match &self.state {
             InternalSolverState::Unsat(core) => Ok(core.clone()),
-            other => Err(SolverError::State(other.to_external(), SolverState::Unsat)),
+            other => Err(StateError {
+                required_state: SolverState::Unsat,
+                actual_state: other.to_external(),
+            }
+            .into()),
         }
     }
 }
@@ -243,20 +248,36 @@ 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) -> Result<(), SolverError> {
+    fn phase_lit(&mut self, lit: Lit) -> anyhow::Result<()> {
         unsafe { ffi::cglucosesimp4_phase(self.handle, lit.to_ipasir()) };
         Ok(())
     }
 
     /// Undoes the effect of a call to [`Glucose::phase_lit`]
-    fn unphase_var(&mut self, var: Var) -> Result<(), SolverError> {
+    fn unphase_var(&mut self, var: Var) -> anyhow::Result<()> {
         unsafe { ffi::cglucosesimp4_unphase(self.handle, var.to_ipasir()) };
         Ok(())
     }
 }
 
+impl FreezeVar for Glucose {
+    fn freeze_var(&mut self, var: Var) -> anyhow::Result<()> {
+        unsafe { ffi::cglucosesimp4_set_frozen(self.handle, var.to_ipasir(), true) };
+        Ok(())
+    }
+
+    fn melt_var(&mut self, var: Var) -> anyhow::Result<()> {
+        unsafe { ffi::cglucosesimp4_set_frozen(self.handle, var.to_ipasir(), false) };
+        Ok(())
+    }
+
+    fn is_frozen(&mut self, var: Var) -> anyhow::Result<bool> {
+        Ok(unsafe { ffi::cglucosesimp4_is_frozen(self.handle, var.to_ipasir()) } != 0)
+    }
+}
+
 impl LimitConflicts for Glucose {
-    fn limit_conflicts(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
+    fn limit_conflicts(&mut self, limit: Option<u32>) -> anyhow::Result<()> {
         self.set_limit(Limit::Conflicts(if let Some(limit) = limit {
             limit as i64
         } else {
@@ -267,7 +288,7 @@ impl LimitConflicts for Glucose {
 }
 
 impl LimitPropagations for Glucose {
-    fn limit_propagations(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
+    fn limit_propagations(&mut self, limit: Option<u32>) -> anyhow::Result<()> {
         self.set_limit(Limit::Propagations(if let Some(limit) = limit {
             limit as i64
         } else {
@@ -421,7 +442,8 @@ mod ffi {
         pub fn cglucosesimp4_set_no_limit(solver: *mut Glucose4Handle);
         pub fn cglucosesimp4_interrupt(solver: *mut Glucose4Handle);
         pub fn cglucosesimp4_set_frozen(solver: *mut Glucose4Handle, var: c_int, frozen: bool);
-        pub fn cglucosesimp4_is_eliminated(solver: *mut Glucose4Handle, var: c_int);
+        pub fn cglucosesimp4_is_frozen(solver: *mut Glucose4Handle, var: c_int) -> c_int;
+        pub fn cglucosesimp4_is_eliminated(solver: *mut Glucose4Handle, var: c_int) -> c_int;
         pub fn cglucosesimp4_propagations(solver: *mut Glucose4Handle) -> u64;
         pub fn cglucosesimp4_decisions(solver: *mut Glucose4Handle) -> u64;
         pub fn cglucosesimp4_conflicts(solver: *mut Glucose4Handle) -> u64;
diff --git a/ipasir/.gitignore b/ipasir/.gitignore
new file mode 100644
index 00000000..4fffb2f8
--- /dev/null
+++ b/ipasir/.gitignore
@@ -0,0 +1,2 @@
+/target
+/Cargo.lock
diff --git a/ipasir/CHANGELOG.md b/ipasir/CHANGELOG.md
new file mode 100644
index 00000000..ba811889
--- /dev/null
+++ b/ipasir/CHANGELOG.md
@@ -0,0 +1,4 @@
+# Changelog
+
+All notable changes to this project will be documented in this file.
+
diff --git a/ipasir/Cargo.toml b/ipasir/Cargo.toml
new file mode 100644
index 00000000..ab859bc1
--- /dev/null
+++ b/ipasir/Cargo.toml
@@ -0,0 +1,18 @@
+[package]
+name = "rustsat-ipasir"
+version = "0.1.0"
+edition = "2021"
+authors = ["Christoph Jabs <christoph.jabs@helsinki.fi>"]
+license = "MIT"
+description = "IPASIR bindings for RustSAT"
+keywords = ["sat-solver", "rustsat"]
+repository = "https://github.com/chrjabs/rustsat"
+readme = "README.md"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+cpu-time = "1.0.0"
+rustsat = { version = "0.4.3", path = "../rustsat", default-features = false }
+thiserror = { version = "1.0.57" }
+anyhow = { version = "1.0.80" }
diff --git a/ipasir/README.md b/ipasir/README.md
new file mode 100644
index 00000000..8254f341
--- /dev/null
+++ b/ipasir/README.md
@@ -0,0 +1,37 @@
+[![Check & Test](https://github.com/chrjabs/rustsat/actions/workflows/ipasir.yml/badge.svg)](https://github.com/chrjabs/rustsat/actions/workflows/ipasir.yml)
+[![crates.io](https://img.shields.io/crates/v/rustsat-ipasir)](https://crates.io/crates/rustsat-ipasir)
+[![docs.rs](https://img.shields.io/docsrs/rustsat-ipasir)](https://docs.rs/rustsat-ipasir)
+[![License](https://img.shields.io/crates/l/rustsat-cadical)](../LICENSE)
+
+<!-- cargo-rdme start -->
+
+# rustsat-ipasir - IPASIR Bindings for RustSAT
+
+[IPASIR](https://github.com/biotomas/ipasir) is a general incremental interface for SAT
+solvers. This crate provides bindings for this API to be used with the
+[RustSAT](https://github.com/chrjabs/rustsat) library.
+
+**Note**: This crate only provides bindings to the API, linking to a IPASIR library needs to be
+set up by the user. This is intentional to allow easy integration of solvers that we do not
+provide a specialized crate for. For a plug-and-play experience see the other rustsat solver
+crates.
+
+## Linking
+
+Linking to a IPASIR library can be done by adding something like the following to your projects
+build script (`build.rs`).
+
+```rust
+// Link to custom IPASIR solver
+// Modify this for linking to your static library
+// The name of the library should be _without_ the prefix 'lib' and the suffix '.a'
+println!("cargo:rustc-link-lib=static=<path-to-your-static-lib>");
+println!("cargo:rustc-link-search=<name-of-your-static-lib>");
+// If your IPASIR solver links to the C++ stdlib, the next four lines are required
+#[cfg(target_os = "macos")]
+println!("cargo:rustc-flags=-l dylib=c++");
+#[cfg(not(target_os = "macos"))]
+println!("cargo:rustc-flags=-l dylib=stdc++");
+```
+
+<!-- cargo-rdme end -->
diff --git a/rustsat/src/solvers/ipasir.rs b/ipasir/src/lib.rs
similarity index 56%
rename from rustsat/src/solvers/ipasir.rs
rename to ipasir/src/lib.rs
index bfe59749..ebe6d5a6 100644
--- a/rustsat/src/solvers/ipasir.rs
+++ b/ipasir/src/lib.rs
@@ -1,17 +1,51 @@
-//! # IPASIR Interface
+//! # rustsat-ipasir - IPASIR Bindings for RustSAT
 //!
-//! Interface to any SAT solver implementing the
-//! [IPASIR API](https://github.com/biotomas/ipasir) for incremental SAT solvers.
+//! [IPASIR](https://github.com/biotomas/ipasir) is a general incremental interface for SAT
+//! solvers. This crate provides bindings for this API to be used with the
+//! [RustSAT](https://github.com/chrjabs/rustsat) library.
+//!
+//! **Note**: This crate only provides bindings to the API, linking to a IPASIR library needs to be
+//! set up by the user. This is intentional to allow easy integration of solvers that we do not
+//! provide a specialized crate for. For a plug-and-play experience see the other rustsat solver
+//! crates.
+//!
+//! ## Linking
+//!
+//! Linking to a IPASIR library can be done by adding something like the following to your projects
+//! build script (`build.rs`).
+//!
+//! ```
+//! // Link to custom IPASIR solver
+//! // Modify this for linking to your static library
+//! // The name of the library should be _without_ the prefix 'lib' and the suffix '.a'
+//! println!("cargo:rustc-link-lib=static=<path-to-your-static-lib>");
+//! println!("cargo:rustc-link-search=<name-of-your-static-lib>");
+//! // If your IPASIR solver links to the C++ stdlib, the next four lines are required
+//! #[cfg(target_os = "macos")]
+//! println!("cargo:rustc-flags=-l dylib=c++");
+//! #[cfg(not(target_os = "macos"))]
+//! println!("cargo:rustc-flags=-l dylib=stdc++");
+//! ```
 
 use core::ffi::{c_int, c_void, CStr};
 
-use super::{
-    ControlSignal, Learn, OptLearnCallbackStore, OptTermCallbackStore, Solve, SolveIncremental,
-    SolveMightFail, SolveStats, SolverError, SolverResult, SolverState, SolverStats, Terminate,
-};
-use crate::types::{Clause, Lit, TernaryVal};
 use cpu_time::ProcessTime;
 use ffi::IpasirHandle;
+use rustsat::{
+    solvers::{
+        ControlSignal, Learn, Solve, SolveIncremental, SolveStats, SolverResult, SolverState,
+        SolverStats, StateError, Terminate,
+    },
+    types::{Clause, Lit, TernaryVal},
+};
+use thiserror::Error;
+
+#[derive(Error, Clone, Copy, PartialEq, Eq, Debug)]
+#[error("ipasir c-api returned an invalid value: {api_call} -> {value}")]
+pub struct InvalidApiReturn {
+    api_call: &'static str,
+    value: c_int,
+}
 
 #[derive(Debug, PartialEq, Eq, Default)]
 #[allow(dead_code)] // Not all solvers use all states
@@ -21,22 +55,26 @@ enum InternalSolverState {
     Input,
     Sat,
     Unsat(Vec<Lit>),
-    Error(String),
 }
 
 impl InternalSolverState {
-    #[cfg(solver)]
     fn to_external(&self) -> SolverState {
         match self {
             InternalSolverState::Configuring => SolverState::Configuring,
             InternalSolverState::Input => SolverState::Input,
             InternalSolverState::Sat => SolverState::Sat,
             InternalSolverState::Unsat(_) => SolverState::Unsat,
-            InternalSolverState::Error(desc) => SolverState::Error(desc.clone()),
         }
     }
 }
 
+type TermCallbackPtr<'a> = Box<dyn FnMut() -> ControlSignal + 'a>;
+type LearnCallbackPtr<'a> = Box<dyn FnMut(Clause) + 'a>;
+/// Double boxing is necessary to get thin pointers for casting
+type OptTermCallbackStore<'a> = Option<Box<TermCallbackPtr<'a>>>;
+/// Double boxing is necessary to get thin pointers for casting
+type OptLearnCallbackStore<'a> = Option<Box<LearnCallbackPtr<'a>>>;
+
 /// Type for an IPASIR solver.
 pub struct IpasirSolver<'term, 'learn> {
     handle: *mut IpasirHandle,
@@ -59,18 +97,18 @@ impl Default for IpasirSolver<'_, '_> {
 }
 
 impl IpasirSolver<'_, '_> {
-    fn get_core_assumps(&self, assumps: &Vec<Lit>) -> Result<Vec<Lit>, SolverError> {
+    fn get_core_assumps(&self, assumps: &[Lit]) -> Result<Vec<Lit>, InvalidApiReturn> {
         let mut core = Vec::new();
         core.reserve(assumps.len());
         for a in assumps {
             match unsafe { ffi::ipasir_failed(self.handle, a.to_ipasir()) } {
                 0 => (),
                 1 => core.push(!*a),
-                invalid => {
-                    return Err(SolverError::Api(format!(
-                        "ipasir_failed returned invalid value: {}",
-                        invalid
-                    )))
+                value => {
+                    return Err(InvalidApiReturn {
+                        api_call: "ipasir_failed",
+                        value,
+                    })
                 }
             }
         }
@@ -87,19 +125,15 @@ impl Solve for IpasirSolver<'_, '_> {
             .expect("IPASIR signature returned invalid UTF-8.")
     }
 
-    fn solve(&mut self) -> Result<SolverResult, SolverError> {
+    fn solve(&mut self) -> anyhow::Result<SolverResult> {
         // If already solved, return state
         if let InternalSolverState::Sat = self.state {
             return Ok(SolverResult::Sat);
-        } else if let InternalSolverState::Unsat(core) = &self.state {
+        }
+        if let InternalSolverState::Unsat(core) = &self.state {
             if core.is_empty() {
                 return Ok(SolverResult::Unsat);
             }
-        } else if let InternalSolverState::Error(desc) = &self.state {
-            return Err(SolverError::State(
-                SolverState::Error(desc.clone()),
-                SolverState::Input,
-            ));
         }
         let start = ProcessTime::now();
         // Solve with IPASIR backend
@@ -121,39 +155,36 @@ impl Solve for IpasirSolver<'_, '_> {
                 self.state = InternalSolverState::Unsat(vec![]);
                 Ok(SolverResult::Unsat)
             }
-            invalid => Err(SolverError::Api(format!(
-                "ipasir_solve returned invalid value: {}",
-                invalid
-            ))),
+            value => Err(InvalidApiReturn {
+                api_call: "ipasir_solve",
+                value,
+            }
+            .into()),
         }
     }
 
-    fn lit_val(&self, lit: Lit) -> Result<TernaryVal, SolverError> {
-        match &self.state {
-            InternalSolverState::Sat => {
-                let lit = lit.to_ipasir();
-                match unsafe { ffi::ipasir_val(self.handle, lit) } {
-                    0 => Ok(TernaryVal::DontCare),
-                    p if p == lit => Ok(TernaryVal::True),
-                    n if n == -lit => Ok(TernaryVal::False),
-                    invalid => Err(SolverError::Api(format!(
-                        "ipasir_val returned invalid value: {}",
-                        invalid
-                    ))),
-                }
+    fn lit_val(&self, lit: Lit) -> anyhow::Result<TernaryVal> {
+        if self.state != InternalSolverState::Sat {
+            return Err(StateError {
+                required_state: SolverState::Sat,
+                actual_state: self.state.to_external(),
+            }
+            .into());
+        }
+        let lit = lit.to_ipasir();
+        match unsafe { ffi::ipasir_val(self.handle, lit) } {
+            0 => Ok(TernaryVal::DontCare),
+            p if p == lit => Ok(TernaryVal::True),
+            n if n == -lit => Ok(TernaryVal::False),
+            value => Err(InvalidApiReturn {
+                api_call: "ipasir_val",
+                value,
             }
-            other => Err(SolverError::State(other.to_external(), SolverState::Sat)),
+            .into()),
         }
     }
 
-    fn add_clause(&mut self, clause: Clause) -> SolveMightFail {
-        if let InternalSolverState::Error(_) = self.state {
-            // Don't add clause if already in error state.
-            return Err(SolverError::State(
-                self.state.to_external(),
-                SolverState::Input,
-            ));
-        }
+    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> {
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         clause.iter().for_each(|l| match self.stats.max_var {
@@ -178,18 +209,12 @@ impl Solve for IpasirSolver<'_, '_> {
 }
 
 impl SolveIncremental for IpasirSolver<'_, '_> {
-    fn solve_assumps(&mut self, assumps: &[Lit]) -> Result<SolverResult, SolverError> {
+    fn solve_assumps(&mut self, assumps: &[Lit]) -> anyhow::Result<SolverResult> {
         // If in error state, remain there
         // If not, need to resolve because assumptions might have changed
-        if let InternalSolverState::Error(desc) = &self.state {
-            return Err(SolverError::State(
-                SolverState::Error(desc.clone()),
-                SolverState::Input,
-            ));
-        }
         let start = ProcessTime::now();
         // Solve with IPASIR backend
-        for a in &assumps {
+        for a in assumps {
             unsafe { ffi::ipasir_assume(self.handle, a.to_ipasir()) }
         }
         let res = unsafe { ffi::ipasir_solve(self.handle) };
@@ -207,20 +232,25 @@ impl SolveIncremental for IpasirSolver<'_, '_> {
             }
             20 => {
                 self.stats.n_unsat += 1;
-                self.state = InternalSolverState::Unsat(self.get_core_assumps(&assumps)?);
+                self.state = InternalSolverState::Unsat(self.get_core_assumps(assumps)?);
                 Ok(SolverResult::Unsat)
             }
-            invalid => Err(SolverError::Api(format!(
-                "ipasir_solve returned invalid value: {}",
-                invalid
-            ))),
+            value => Err(InvalidApiReturn {
+                api_call: "ipasir_solve",
+                value,
+            }
+            .into()),
         }
     }
 
-    fn core(&mut self) -> Result<Vec<Lit>, SolverError> {
+    fn core(&mut self) -> anyhow::Result<Vec<Lit>> {
         match &self.state {
             InternalSolverState::Unsat(core) => Ok(core.clone()),
-            other => Err(SolverError::State(other.to_external(), SolverState::Unsat)),
+            other => Err(StateError {
+                required_state: SolverState::Unsat,
+                actual_state: other.to_external(),
+            }
+            .into()),
         }
     }
 }
@@ -232,8 +262,9 @@ impl<'term> Terminate<'term> for IpasirSolver<'term, '_> {
     ///
     /// Terminate solver after 10 callback calls.
     ///
-    /// ```
-    /// use rustsat::solvers::{IpasirSolver, ControlSignal, Solve, SolverResult, Terminate};
+    /// ```no_run
+    /// use rustsat::solvers::{ControlSignal, Solve, SolverResult, Terminate};
+    /// use rustsat_ipasir::IpasirSolver;
     ///
     /// let mut solver = IpasirSolver::default();
     ///
@@ -260,14 +291,12 @@ impl<'term> Terminate<'term> for IpasirSolver<'term, '_> {
     {
         self.terminate_cb = Some(Box::new(Box::new(cb)));
         let cb_ptr = self.terminate_cb.as_mut().unwrap().as_mut() as *const _ as *const c_void;
-        unsafe { ffi::ipasir_set_terminate(self.handle, cb_ptr, ffi::ipasir_terminate_cb) }
+        unsafe { ffi::ipasir_set_terminate(self.handle, cb_ptr, Some(ffi::ipasir_terminate_cb)) }
     }
 
     fn detach_terminator(&mut self) {
         self.terminate_cb = None;
-        let null_cb: extern "C" fn(*const c_void) -> c_int =
-            unsafe { std::mem::transmute(std::ptr::null::<u32>()) };
-        unsafe { ffi::ipasir_set_terminate(self.handle, std::ptr::null(), null_cb) }
+        unsafe { ffi::ipasir_set_terminate(self.handle, std::ptr::null(), None) }
     }
 }
 
@@ -280,8 +309,9 @@ impl<'learn> Learn<'learn> for IpasirSolver<'_, 'learn> {
     ///
     /// Count number of learned clauses up to length 10.
     ///
-    /// ```
-    /// use rustsat::solvers::{IpasirSolver, Solve, SolverResult, Learn};
+    /// ```no_run
+    /// use rustsat::solvers::{Solve, SolverResult, Learn};
+    /// use rustsat_ipasir::IpasirSolver;
     ///
     /// let mut cnt = 0;
     ///
@@ -307,16 +337,14 @@ impl<'learn> Learn<'learn> for IpasirSolver<'_, 'learn> {
                 self.handle,
                 cb_ptr,
                 max_len.try_into().unwrap(),
-                ffi::ipasir_learn_cb,
+                Some(ffi::ipasir_learn_cb),
             )
         }
     }
 
     fn detach_learner(&mut self) {
         self.terminate_cb = None;
-        let null_cb: extern "C" fn(*const c_void, *const c_int) =
-            unsafe { std::mem::transmute(std::ptr::null::<u32>()) };
-        unsafe { ffi::ipasir_set_learn(self.handle, std::ptr::null(), 0, null_cb) }
+        unsafe { ffi::ipasir_set_learn(self.handle, std::ptr::null(), 0, None) }
     }
 }
 
@@ -332,124 +360,18 @@ impl Drop for IpasirSolver<'_, '_> {
     }
 }
 
-#[cfg(test)]
-mod test {
-    use super::IpasirSolver;
-    use crate::{
-        lit,
-        solvers::{ControlSignal, Learn, Solve, SolverResult, Terminate},
-        types::Lit,
-    };
-
-    #[test]
-    fn build_destroy() {
-        let _solver = IpasirSolver::default();
-    }
-
-    #[test]
-    fn build_two() {
-        let _solver1 = IpasirSolver::default();
-        let _solver2 = IpasirSolver::default();
-    }
-
-    #[test]
-    fn tiny_instance_sat() {
-        let mut solver = IpasirSolver::default();
-        solver.add_binary(lit![0], !lit![1]).unwrap();
-        solver.add_binary(lit![1], !lit![2]).unwrap();
-        let ret = solver.solve();
-        match ret {
-            Err(e) => panic!("got error when solving: {}", e),
-            Ok(res) => assert_eq!(res, SolverResult::Sat),
-        }
-    }
-
-    #[test]
-    fn tiny_instance_unsat() {
-        let mut solver = IpasirSolver::default();
-        solver.add_unit(!lit![0]).unwrap();
-        solver.add_binary(lit![0], !lit![1]).unwrap();
-        solver.add_binary(lit![1], !lit![2]).unwrap();
-        solver.add_unit(lit![2]).unwrap();
-        let ret = solver.solve();
-        match ret {
-            Err(e) => panic!("got error when solving: {}", e),
-            Ok(res) => assert_eq!(res, SolverResult::Unsat),
-        }
-    }
-
-    #[test]
-    fn termination_callback() {
-        let mut solver = IpasirSolver::default();
-        solver.add_binary(lit![0], !lit![1]).unwrap();
-        solver.add_binary(lit![1], !lit![2]).unwrap();
-        solver.add_binary(lit![2], !lit![3]).unwrap();
-        solver.add_binary(lit![3], !lit![4]).unwrap();
-        solver.add_binary(lit![4], !lit![5]).unwrap();
-        solver.add_binary(lit![5], !lit![6]).unwrap();
-        solver.add_binary(lit![6], !lit![7]).unwrap();
-        solver.add_binary(lit![7], !lit![8]).unwrap();
-        solver.add_binary(lit![8], !lit![9]).unwrap();
-
-        solver.attach_terminator(|| ControlSignal::Terminate);
-
-        let ret = solver.solve();
-
-        match ret {
-            Err(e) => panic!("got error when solving: {}", e),
-            Ok(res) => assert_eq!(res, SolverResult::Interrupted),
-        }
-
-        // Note: since IPASIR doesn't specify _when_ the terminator callback needs
-        // to be called, there is no guarantee that the callback is actually
-        // called during solving. This might cause this test to fail with some solvers.
-    }
-
-    #[test]
-    fn learner_callback() {
-        let mut solver = IpasirSolver::default();
-        solver.add_binary(lit![0], !lit![1]).unwrap();
-        solver.add_binary(lit![1], !lit![2]).unwrap();
-        solver.add_binary(lit![2], !lit![3]).unwrap();
-        solver.add_binary(lit![3], !lit![4]).unwrap();
-        solver.add_binary(lit![4], !lit![5]).unwrap();
-        solver.add_binary(lit![5], !lit![6]).unwrap();
-        solver.add_binary(lit![6], !lit![7]).unwrap();
-        solver.add_binary(lit![7], !lit![8]).unwrap();
-        solver.add_binary(lit![8], !lit![9]).unwrap();
-        solver.add_unit(lit![9]).unwrap();
-        solver.add_unit(!lit![0]).unwrap();
-
-        let mut cl_len = 0;
-        let ret;
-
-        solver.attach_learner(
-            |clause| {
-                cl_len = clause.len();
-            },
-            10,
-        );
-
-        ret = solver.solve();
-
-        drop(solver);
-
-        // Note: it is hard to create a testing instance on which clause learning
-        // actually happens and therefore it is not actually tested if the
-        // callback is called
-
-        match ret {
-            Err(e) => panic!("got error when solving: {}", e),
-            Ok(res) => assert_eq!(res, SolverResult::Unsat),
-        }
+impl Extend<Clause> for IpasirSolver<'_, '_> {
+    fn extend<T: IntoIterator<Item = Clause>>(&mut self, iter: T) {
+        iter.into_iter()
+            .for_each(|cl| self.add_clause(cl).expect("Error adding clause in extend"))
     }
 }
 
 /// cbindgen:ignore
 mod ffi {
-    use crate::solvers::{ControlSignal, LearnCallbackPtr, TermCallbackPtr};
-    use crate::types::Lit;
+    use super::{LearnCallbackPtr, TermCallbackPtr};
     use core::ffi::{c_char, c_int, c_void};
+    use rustsat::{solvers::ControlSignal, types::Lit};
     use std::slice;
 
     #[repr(C)]
@@ -470,13 +392,13 @@ mod ffi {
         pub fn ipasir_set_terminate(
             solver: *mut IpasirHandle,
             state: *const c_void,
-            terminate: extern "C" fn(state: *const c_void) -> c_int,
+            terminate: Option<extern "C" fn(state: *const c_void) -> c_int>,
         );
         pub fn ipasir_set_learn(
             solver: *mut IpasirHandle,
             state: *const c_void,
             max_length: c_int,
-            learn: extern "C" fn(state: *const c_void, clause: *const c_int),
+            learn: Option<extern "C" fn(state: *const c_void, clause: *const c_int)>,
         );
     }
 
diff --git a/kissat/Cargo.toml b/kissat/Cargo.toml
index bd0e738c..cf0817c4 100644
--- a/kissat/Cargo.toml
+++ b/kissat/Cargo.toml
@@ -27,6 +27,8 @@ sc2022-bulky = []
 [dependencies]
 cpu-time = "1.0.0"
 rustsat = { version = "0.4.3", path = "../rustsat", default-features = false }
+thiserror = { version = "1.0.57" }
+anyhow = { version = "1.0.80" }
 
 [build-dependencies]
 cc = { version = "1.0.83", features = ["parallel"] }
diff --git a/kissat/src/lib.rs b/kissat/src/lib.rs
index d6ca2d5b..317eda81 100644
--- a/kissat/src/lib.rs
+++ b/kissat/src/lib.rs
@@ -30,11 +30,19 @@ use cpu_time::ProcessTime;
 use ffi::KissatHandle;
 use rustsat::{
     solvers::{
-        ControlSignal, Interrupt, InterruptSolver, Solve, SolveMightFail, SolveStats, SolverError,
-        SolverResult, SolverState, SolverStats, Terminate,
+        ControlSignal, Interrupt, InterruptSolver, Solve, SolveStats, SolverResult, SolverState,
+        SolverStats, StateError, Terminate,
     },
     types::{Clause, Lit, TernaryVal, Var},
 };
+use thiserror::Error;
+
+#[derive(Error, Clone, Copy, PartialEq, Eq, Debug)]
+#[error("kissat c-api returned an invalid value: {api_call} -> {value}")]
+pub struct InvalidApiReturn {
+    api_call: &'static str,
+    value: c_int,
+}
 
 #[derive(Debug, PartialEq, Eq, Default)]
 enum InternalSolverState {
@@ -43,7 +51,6 @@ enum InternalSolverState {
     Input,
     Sat,
     Unsat(Vec<Lit>),
-    Error(String),
 }
 
 impl InternalSolverState {
@@ -53,7 +60,6 @@ impl InternalSolverState {
             InternalSolverState::Input => SolverState::Input,
             InternalSolverState::Sat => SolverState::Sat,
             InternalSolverState::Unsat(_) => SolverState::Unsat,
-            InternalSolverState::Error(desc) => SolverState::Error(desc.clone()),
         }
     }
 }
@@ -111,62 +117,51 @@ impl Kissat<'_> {
     }
 
     /// Sets a pre-defined configuration for Kissat's internal options
-    pub fn set_configuration(&mut self, config: Config) -> SolveMightFail {
-        if self.state == InternalSolverState::Configuring {
-            let config_name = match config {
-                Config::Default => CString::new("default").unwrap(),
-                Config::Basic => CString::new("basic").unwrap(),
-                Config::Plain => CString::new("plain").unwrap(),
-                Config::SAT => CString::new("sat").unwrap(),
-                Config::UNSAT => CString::new("unsat").unwrap(),
-            };
-            let ret = unsafe { ffi::kissat_set_configuration(self.handle, config_name.as_ptr()) };
-            if ret != 0 {
-                Ok(())
-            } else {
-                Err(SolverError::Api("kissat_configure returned 0".to_string()))
+    pub fn set_configuration(&mut self, config: Config) -> anyhow::Result<()> {
+        if self.state != InternalSolverState::Configuring {
+            return Err(StateError {
+                required_state: SolverState::Configuring,
+                actual_state: self.state.to_external(),
             }
+            .into());
+        }
+        let config_name = match config {
+            Config::Default => CString::new("default").unwrap(),
+            Config::Basic => CString::new("basic").unwrap(),
+            Config::Plain => CString::new("plain").unwrap(),
+            Config::SAT => CString::new("sat").unwrap(),
+            Config::UNSAT => CString::new("unsat").unwrap(),
+        };
+        let ret = unsafe { ffi::kissat_set_configuration(self.handle, config_name.as_ptr()) };
+        if ret != 0 {
+            Ok(())
         } else {
-            Err(SolverError::State(
-                self.state.to_external(),
-                SolverState::Configuring,
-            ))
+            Err(InvalidApiReturn {
+                api_call: "kissat_configure",
+                value: 0,
+            }
+            .into())
         }
     }
 
     /// Sets the value of a Kissat option. For possible options, check Kissat with `kissat --help`.
     /// Requires state [`SolverState::Configuring`].
-    pub fn set_option(&mut self, name: &str, value: c_int) -> SolveMightFail {
-        let c_name = match CString::new(name) {
-            Ok(cstr) => cstr,
-            Err(_) => {
-                return Err(SolverError::Api(format!(
-                    "Kissat option {} cannot be converted to a C string",
-                    name
-                )))
-            }
-        };
+    pub fn set_option(&mut self, name: &str, value: c_int) -> anyhow::Result<()> {
+        let c_name = CString::new(name)?;
         if unsafe { ffi::kissat_set_option(self.handle, c_name.as_ptr(), value) } != 0 {
             Ok(())
         } else {
-            Err(SolverError::Api(format!(
-                "kissat_set_option returned false for option {}",
-                name
-            )))
+            Err(InvalidApiReturn {
+                api_call: "kissat_set_option",
+                value: 0,
+            }
+            .into())
         }
     }
 
     /// Gets the value of a Kissat option. For possible options, check Kissat with `kissat --help`.
-    pub fn get_option(&self, name: &str) -> Result<c_int, SolverError> {
-        let c_name = match CString::new(name) {
-            Ok(cstr) => cstr,
-            Err(_) => {
-                return Err(SolverError::Api(format!(
-                    "Kissat option {} cannot be converted to a C string",
-                    name
-                )))
-            }
-        };
+    pub fn get_option(&self, name: &str) -> anyhow::Result<c_int> {
+        let c_name = CString::new(name)?;
         Ok(unsafe { ffi::kissat_get_option(self.handle, c_name.as_ptr()) })
     }
 
@@ -200,31 +195,19 @@ impl Solve for Kissat<'_> {
             .expect("Kissat signature returned invalid UTF-8.")
     }
 
-    fn reserve(&mut self, max_var: Var) -> SolveMightFail {
-        self.state = match self.state {
-            InternalSolverState::Error(_) => {
-                return Err(SolverError::State(
-                    self.state.to_external(),
-                    SolverState::Input,
-                ))
-            }
-            _ => InternalSolverState::Input,
-        };
+    fn reserve(&mut self, max_var: Var) -> anyhow::Result<()> {
+        self.state = InternalSolverState::Input;
         unsafe { ffi::kissat_reserve(self.handle, max_var.to_ipasir()) };
         Ok(())
     }
 
-    fn solve(&mut self) -> Result<SolverResult, SolverError> {
+    fn solve(&mut self) -> anyhow::Result<SolverResult> {
         // If already solved, return state
         if let InternalSolverState::Sat = self.state {
             return Ok(SolverResult::Sat);
-        } else if let InternalSolverState::Unsat(_) = self.state {
+        }
+        if let InternalSolverState::Unsat(_) = self.state {
             return Ok(SolverResult::Unsat);
-        } else if let InternalSolverState::Error(desc) = &self.state {
-            return Err(SolverError::State(
-                SolverState::Error(desc.clone()),
-                SolverState::Input,
-            ));
         }
         let start = ProcessTime::now();
         // Solve with Kissat backend
@@ -246,49 +229,46 @@ impl Solve for Kissat<'_> {
                 self.state = InternalSolverState::Unsat(vec![]);
                 Ok(SolverResult::Unsat)
             }
-            invalid => Err(SolverError::Api(format!(
-                "kissat_solve returned invalid value: {}",
-                invalid
-            ))),
+            value => Err(InvalidApiReturn {
+                api_call: "kissat_solve",
+                value,
+            }
+            .into()),
         }
     }
 
-    fn lit_val(&self, lit: Lit) -> Result<TernaryVal, SolverError> {
-        match &self.state {
-            InternalSolverState::Sat => {
-                let lit = lit.to_ipasir();
-                match unsafe { ffi::kissat_value(self.handle, lit) } {
-                    0 => Ok(TernaryVal::DontCare),
-                    p if p == lit => Ok(TernaryVal::True),
-                    n if n == -lit => Ok(TernaryVal::False),
-                    invalid => Err(SolverError::Api(format!(
-                        "kissat_val returned invalid value: {}",
-                        invalid
-                    ))),
-                }
+    fn lit_val(&self, lit: Lit) -> anyhow::Result<TernaryVal> {
+        if self.state != InternalSolverState::Sat {
+            return Err(StateError {
+                required_state: SolverState::Sat,
+                actual_state: self.state.to_external(),
+            }
+            .into());
+        }
+        let lit = lit.to_ipasir();
+        match unsafe { ffi::kissat_value(self.handle, lit) } {
+            0 => Ok(TernaryVal::DontCare),
+            p if p == lit => Ok(TernaryVal::True),
+            n if n == -lit => Ok(TernaryVal::False),
+            value => Err(InvalidApiReturn {
+                api_call: "kissat_value",
+                value,
             }
-            other => Err(SolverError::State(other.to_external(), SolverState::Sat)),
+            .into()),
         }
     }
 
-    fn add_clause(&mut self, clause: Clause) -> SolveMightFail {
+    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> {
         // Kissat is non-incremental, so only add if in input or configuring state
-        match &mut self.state {
-            InternalSolverState::Input | InternalSolverState::Configuring => (),
-            InternalSolverState::Error(_) => {
-                return Err(SolverError::State(
-                    self.state.to_external(),
-                    SolverState::Input,
-                ))
-            }
-            other => {
-                let old_state = other.to_external();
-                // Transition into error state
-                *other = InternalSolverState::Error(String::from(
-                    "added clause while not in input state",
-                ));
-                return Err(SolverError::State(old_state, SolverState::Input));
+        if !matches!(
+            self.state,
+            InternalSolverState::Input | InternalSolverState::Configuring
+        ) {
+            return Err(StateError {
+                required_state: SolverState::Input,
+                actual_state: self.state.to_external(),
             }
+            .into());
         }
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
@@ -445,7 +425,7 @@ mod test {
     use super::{Config, Kissat, Limit};
     use rustsat::{
         lit,
-        solvers::{Solve, SolverError, SolverResult, SolverState},
+        solvers::{Solve, SolverResult, SolverState, StateError},
     };
 
     #[test]
@@ -494,13 +474,13 @@ mod test {
         solver.set_configuration(Config::SAT).unwrap();
         solver.set_configuration(Config::UNSAT).unwrap();
         solver.add_unit(lit![0]).unwrap();
-        assert_eq!(
-            solver.set_configuration(Config::Default),
-            Err(SolverError::State(
-                SolverState::Input,
-                SolverState::Configuring
-            ))
-        );
+        assert!(solver.set_configuration(Config::Default).is_err_and(|e| e
+            .downcast::<StateError>()
+            .unwrap()
+            == StateError {
+                required_state: SolverState::Configuring,
+                actual_state: SolverState::Input
+            }));
     }
 
     #[test]
diff --git a/minisat/Cargo.toml b/minisat/Cargo.toml
index a47f3eec..ace5a5b1 100644
--- a/minisat/Cargo.toml
+++ b/minisat/Cargo.toml
@@ -21,6 +21,8 @@ default = ["quiet"]
 [dependencies]
 cpu-time = "1.0.0"
 rustsat = { version = "0.4.3", path = "../rustsat", default-features = false }
+thiserror = { version = "1.0.57" }
+anyhow = { version = "1.0.80" }
 
 [build-dependencies]
 cc = { version = "1.0.83", features = ["parallel"] }
diff --git a/minisat/build.rs b/minisat/build.rs
index 35778969..8c3850d0 100644
--- a/minisat/build.rs
+++ b/minisat/build.rs
@@ -11,7 +11,7 @@ fn main() {
     build(
         "https://github.com/chrjabs/minisat.git",
         "master",
-        "8237c54e97272d16531e785dd8031c27c2360904",
+        "f91df3ab8f9eeaebe351f4a1890cf92831b8b636",
     );
 
     let out_dir = env::var("OUT_DIR").unwrap();
diff --git a/minisat/src/core.rs b/minisat/src/core.rs
index 37b7ffdc..f02531c1 100644
--- a/minisat/src/core.rs
+++ b/minisat/src/core.rs
@@ -5,14 +5,13 @@
 
 use core::ffi::{c_int, CStr};
 
-use super::{InternalSolverState, Limit};
+use super::{InternalSolverState, InvalidApiReturn, Limit};
 use cpu_time::ProcessTime;
 use ffi::MinisatHandle;
 use rustsat::{
     solvers::{
         GetInternalStats, Interrupt, InterruptSolver, LimitConflicts, LimitPropagations, PhaseLit,
-        Solve, SolveIncremental, SolveMightFail, SolveStats, SolverError, SolverResult,
-        SolverState, SolverStats,
+        Solve, SolveIncremental, SolveStats, SolverResult, SolverState, SolverStats, StateError,
     },
     types::{Clause, Lit, TernaryVal, Var},
 };
@@ -35,17 +34,17 @@ impl Default for Minisat {
 }
 
 impl Minisat {
-    fn get_core_assumps(&self, assumps: &[Lit]) -> Result<Vec<Lit>, SolverError> {
+    fn get_core_assumps(&self, assumps: &[Lit]) -> Result<Vec<Lit>, InvalidApiReturn> {
         let mut core = Vec::new();
         for a in assumps {
             match unsafe { ffi::cminisat_failed(self.handle, a.to_ipasir()) } {
                 0 => (),
                 1 => core.push(!*a),
-                invalid => {
-                    return Err(SolverError::Api(format!(
-                        "cminisat_failed returned invalid value: {}",
-                        invalid
-                    )))
+                value => {
+                    return Err(InvalidApiReturn {
+                        api_call: "cminisat_failed",
+                        value,
+                    })
                 }
             }
         }
@@ -90,11 +89,12 @@ impl Solve for Minisat {
             .expect("Minisat signature returned invalid UTF-8.")
     }
 
-    fn solve(&mut self) -> Result<SolverResult, SolverError> {
+    fn solve(&mut self) -> anyhow::Result<SolverResult> {
         // If already solved, return state
         if let InternalSolverState::Sat = self.state {
             return Ok(SolverResult::Sat);
-        } else if let InternalSolverState::Unsat(core) = &self.state {
+        }
+        if let InternalSolverState::Unsat(core) = &self.state {
             if core.is_empty() {
                 return Ok(SolverResult::Unsat);
             }
@@ -119,32 +119,36 @@ impl Solve for Minisat {
                 self.state = InternalSolverState::Unsat(vec![]);
                 Ok(SolverResult::Unsat)
             }
-            invalid => Err(SolverError::Api(format!(
-                "cminisat_solve returned invalid value: {}",
-                invalid
-            ))),
+            value => Err(InvalidApiReturn {
+                api_call: "cminisat_solve",
+                value,
+            }
+            .into()),
         }
     }
 
-    fn lit_val(&self, lit: Lit) -> Result<TernaryVal, SolverError> {
-        match &self.state {
-            InternalSolverState::Sat => {
-                let lit = lit.to_ipasir();
-                match unsafe { ffi::cminisat_val(self.handle, lit) } {
-                    0 => Ok(TernaryVal::DontCare),
-                    p if p == lit => Ok(TernaryVal::True),
-                    n if n == -lit => Ok(TernaryVal::False),
-                    invalid => Err(SolverError::Api(format!(
-                        "cminisat_val returned invalid value: {}",
-                        invalid
-                    ))),
-                }
+    fn lit_val(&self, lit: Lit) -> anyhow::Result<TernaryVal> {
+        if self.state != InternalSolverState::Sat {
+            return Err(StateError {
+                required_state: SolverState::Sat,
+                actual_state: self.state.to_external(),
             }
-            other => Err(SolverError::State(other.to_external(), SolverState::Sat)),
+            .into());
+        }
+        let lit = lit.to_ipasir();
+        match unsafe { ffi::cminisat_val(self.handle, lit) } {
+            0 => Ok(TernaryVal::DontCare),
+            p if p == lit => Ok(TernaryVal::True),
+            n if n == -lit => Ok(TernaryVal::False),
+            value => Err(InvalidApiReturn {
+                api_call: "cminisat_val",
+                value,
+            }
+            .into()),
         }
     }
 
-    fn add_clause(&mut self, clause: Clause) -> SolveMightFail {
+    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> {
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         self.stats.avg_clause_len =
@@ -161,7 +165,7 @@ impl Solve for Minisat {
 }
 
 impl SolveIncremental for Minisat {
-    fn solve_assumps(&mut self, assumps: &[Lit]) -> Result<SolverResult, SolverError> {
+    fn solve_assumps(&mut self, assumps: &[Lit]) -> anyhow::Result<SolverResult> {
         let start = ProcessTime::now();
         // Solve with minisat backend
         for a in assumps {
@@ -185,17 +189,22 @@ impl SolveIncremental for Minisat {
                 self.state = InternalSolverState::Unsat(self.get_core_assumps(assumps)?);
                 Ok(SolverResult::Unsat)
             }
-            invalid => Err(SolverError::Api(format!(
-                "cminisat_solve returned invalid value: {}",
-                invalid
-            ))),
+            value => Err(InvalidApiReturn {
+                api_call: "cminisat_solve",
+                value,
+            }
+            .into()),
         }
     }
 
-    fn core(&mut self) -> Result<Vec<Lit>, SolverError> {
+    fn core(&mut self) -> anyhow::Result<Vec<Lit>> {
         match &self.state {
             InternalSolverState::Unsat(core) => Ok(core.clone()),
-            other => Err(SolverError::State(other.to_external(), SolverState::Unsat)),
+            other => Err(StateError {
+                required_state: SolverState::Unsat,
+                actual_state: other.to_external(),
+            }
+            .into()),
         }
     }
 }
@@ -226,20 +235,20 @@ 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) -> Result<(), SolverError> {
+    fn phase_lit(&mut self, lit: Lit) -> anyhow::Result<()> {
         unsafe { ffi::cminisat_phase(self.handle, lit.to_ipasir()) };
         Ok(())
     }
 
     /// Undoes the effect of a call to [`Minisat::phase_lit`]
-    fn unphase_var(&mut self, var: Var) -> Result<(), SolverError> {
+    fn unphase_var(&mut self, var: Var) -> anyhow::Result<()> {
         unsafe { ffi::cminisat_unphase(self.handle, var.to_ipasir()) };
         Ok(())
     }
 }
 
 impl LimitConflicts for Minisat {
-    fn limit_conflicts(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
+    fn limit_conflicts(&mut self, limit: Option<u32>) -> anyhow::Result<()> {
         self.set_limit(Limit::Conflicts(if let Some(limit) = limit {
             limit as i64
         } else {
@@ -250,7 +259,7 @@ impl LimitConflicts for Minisat {
 }
 
 impl LimitPropagations for Minisat {
-    fn limit_propagations(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
+    fn limit_propagations(&mut self, limit: Option<u32>) -> anyhow::Result<()> {
         self.set_limit(Limit::Propagations(if let Some(limit) = limit {
             limit as i64
         } else {
diff --git a/minisat/src/lib.rs b/minisat/src/lib.rs
index a7d1a679..ea228a29 100644
--- a/minisat/src/lib.rs
+++ b/minisat/src/lib.rs
@@ -12,12 +12,26 @@
 //! The version of minisat in this crate is Version 2.2.0.
 //! The used C++ source repository can be found [here](https://github.com/chrjabs/minisat).
 
-use rustsat::{solvers::SolverState, types::Lit};
-use std::fmt;
+use rustsat::{
+    solvers::SolverState,
+    types::{Lit, Var},
+};
+use std::{ffi::c_int, fmt};
+use thiserror::Error;
 
+pub mod core;
 pub mod simp;
 
-pub mod core;
+#[derive(Error, Clone, Copy, PartialEq, Eq, Debug)]
+#[error("minisat c-api returned an invalid value: {api_call} -> {value}")]
+pub struct InvalidApiReturn {
+    api_call: &'static str,
+    value: c_int,
+}
+
+#[derive(Error, Clone, Copy, PartialEq, Eq, Debug)]
+#[error("assumption variable {0} has been eliminated by minisat simplification")]
+pub struct AssumpEliminated(Var);
 
 #[derive(Debug, PartialEq, Eq, Default)]
 enum InternalSolverState {
diff --git a/minisat/src/simp.rs b/minisat/src/simp.rs
index 81c7528c..3492fae1 100644
--- a/minisat/src/simp.rs
+++ b/minisat/src/simp.rs
@@ -5,14 +5,14 @@
 
 use core::ffi::{c_int, CStr};
 
-use super::{InternalSolverState, Limit};
+use super::{AssumpEliminated, InternalSolverState, InvalidApiReturn, Limit};
 use cpu_time::ProcessTime;
 use ffi::MinisatHandle;
 use rustsat::{
     solvers::{
-        GetInternalStats, Interrupt, InterruptSolver, LimitConflicts, LimitPropagations, PhaseLit,
-        Solve, SolveIncremental, SolveMightFail, SolveStats, SolverError, SolverResult,
-        SolverState, SolverStats,
+        FreezeVar, GetInternalStats, Interrupt, InterruptSolver, LimitConflicts, LimitPropagations,
+        PhaseLit, Solve, SolveIncremental, SolveStats, SolverResult, SolverState, SolverStats,
+        StateError,
     },
     types::{Clause, Lit, TernaryVal, Var},
 };
@@ -35,17 +35,17 @@ impl Default for Minisat {
 }
 
 impl Minisat {
-    fn get_core_assumps(&self, assumps: &[Lit]) -> Result<Vec<Lit>, SolverError> {
+    fn get_core_assumps(&self, assumps: &[Lit]) -> Result<Vec<Lit>, InvalidApiReturn> {
         let mut core = Vec::new();
         for a in assumps {
             match unsafe { ffi::cminisatsimp_failed(self.handle, a.to_ipasir()) } {
                 0 => (),
                 1 => core.push(!*a),
-                invalid => {
-                    return Err(SolverError::Api(format!(
-                        "cminisatsimp_failed returned invalid value: {}",
-                        invalid
-                    )))
+                value => {
+                    return Err(InvalidApiReturn {
+                        api_call: "cminisatsimp_failed",
+                        value,
+                    })
                 }
             }
         }
@@ -75,19 +75,9 @@ impl Minisat {
         unsafe { ffi::cminisatsimp_n_learnts(self.handle) }
     }
 
-    /// Freezes a literal.
-    pub fn freeze_lit(&mut self, lit: Lit) {
-        unsafe { ffi::cminisatsimp_set_frozen(self.handle, lit.var().to_ipasir(), true) }
-    }
-
-    /// Melts a literal.
-    pub fn melt_lit(&mut self, lit: Lit) {
-        unsafe { ffi::cminisatsimp_set_frozen(self.handle, lit.var().to_ipasir(), false) }
-    }
-
     /// Checks if a variable has been eliminated by preprocessing.
-    pub fn var_eliminated(&mut self, var: Var) {
-        unsafe { ffi::cminisatsimp_is_eliminated(self.handle, var.to_ipasir()) }
+    pub fn var_eliminated(&mut self, var: Var) -> bool {
+        (unsafe { ffi::cminisatsimp_is_eliminated(self.handle, var.to_ipasir()) } != 0)
     }
 }
 
@@ -107,11 +97,12 @@ impl Solve for Minisat {
             .expect("Minisat signature returned invalid UTF-8.")
     }
 
-    fn solve(&mut self) -> Result<SolverResult, SolverError> {
+    fn solve(&mut self) -> anyhow::Result<SolverResult> {
         // If already solved, return state
         if let InternalSolverState::Sat = self.state {
             return Ok(SolverResult::Sat);
-        } else if let InternalSolverState::Unsat(core) = &self.state {
+        }
+        if let InternalSolverState::Unsat(core) = &self.state {
             if core.is_empty() {
                 return Ok(SolverResult::Unsat);
             }
@@ -136,32 +127,36 @@ impl Solve for Minisat {
                 self.state = InternalSolverState::Unsat(vec![]);
                 Ok(SolverResult::Unsat)
             }
-            invalid => Err(SolverError::Api(format!(
-                "cminisatsimp_solve returned invalid value: {}",
-                invalid
-            ))),
+            value => Err(InvalidApiReturn {
+                api_call: "cminisatsimp_solve",
+                value,
+            }
+            .into()),
         }
     }
 
-    fn lit_val(&self, lit: Lit) -> Result<TernaryVal, SolverError> {
-        match &self.state {
-            InternalSolverState::Sat => {
-                let lit = lit.to_ipasir();
-                match unsafe { ffi::cminisatsimp_val(self.handle, lit) } {
-                    0 => Ok(TernaryVal::DontCare),
-                    p if p == lit => Ok(TernaryVal::True),
-                    n if n == -lit => Ok(TernaryVal::False),
-                    invalid => Err(SolverError::Api(format!(
-                        "cminisatsimp_val returned invalid value: {}",
-                        invalid
-                    ))),
-                }
+    fn lit_val(&self, lit: Lit) -> anyhow::Result<TernaryVal> {
+        if self.state != InternalSolverState::Sat {
+            return Err(StateError {
+                required_state: SolverState::Sat,
+                actual_state: self.state.to_external(),
+            }
+            .into());
+        }
+        let lit = lit.to_ipasir();
+        match unsafe { ffi::cminisatsimp_val(self.handle, lit) } {
+            0 => Ok(TernaryVal::DontCare),
+            p if p == lit => Ok(TernaryVal::True),
+            n if n == -lit => Ok(TernaryVal::False),
+            value => Err(InvalidApiReturn {
+                api_call: "cminisatsimp_val",
+                value,
             }
-            other => Err(SolverError::State(other.to_external(), SolverState::Sat)),
+            .into()),
         }
     }
 
-    fn add_clause(&mut self, clause: Clause) -> SolveMightFail {
+    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> {
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         self.stats.avg_clause_len =
@@ -178,9 +173,14 @@ impl Solve for Minisat {
 }
 
 impl SolveIncremental for Minisat {
-    fn solve_assumps(&mut self, assumps: &[Lit]) -> Result<SolverResult, SolverError> {
+    fn solve_assumps(&mut self, assumps: &[Lit]) -> anyhow::Result<SolverResult> {
         let start = ProcessTime::now();
         // Solve with minisat backend
+        for a in assumps {
+            if self.var_eliminated(a.var()) {
+                return Err(AssumpEliminated(a.var()).into());
+            }
+        }
         for a in assumps {
             unsafe { ffi::cminisatsimp_assume(self.handle, a.to_ipasir()) }
         }
@@ -202,17 +202,22 @@ impl SolveIncremental for Minisat {
                 self.state = InternalSolverState::Unsat(self.get_core_assumps(assumps)?);
                 Ok(SolverResult::Unsat)
             }
-            invalid => Err(SolverError::Api(format!(
-                "cminisatsimp_solve returned invalid value: {}",
-                invalid
-            ))),
+            value => Err(InvalidApiReturn {
+                api_call: "cminisatsimp_solve",
+                value,
+            }
+            .into()),
         }
     }
 
-    fn core(&mut self) -> Result<Vec<Lit>, SolverError> {
+    fn core(&mut self) -> anyhow::Result<Vec<Lit>> {
         match &self.state {
             InternalSolverState::Unsat(core) => Ok(core.clone()),
-            other => Err(SolverError::State(other.to_external(), SolverState::Unsat)),
+            other => Err(StateError {
+                required_state: SolverState::Unsat,
+                actual_state: other.to_external(),
+            }
+            .into()),
         }
     }
 }
@@ -243,20 +248,36 @@ 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) -> Result<(), SolverError> {
+    fn phase_lit(&mut self, lit: Lit) -> anyhow::Result<()> {
         unsafe { ffi::cminisatsimp_phase(self.handle, lit.to_ipasir()) };
         Ok(())
     }
 
     /// Undoes the effect of a call to [`Minisat::phase_lit`]
-    fn unphase_var(&mut self, var: Var) -> Result<(), SolverError> {
+    fn unphase_var(&mut self, var: Var) -> anyhow::Result<()> {
         unsafe { ffi::cminisatsimp_unphase(self.handle, var.to_ipasir()) };
         Ok(())
     }
 }
 
+impl FreezeVar for Minisat {
+    fn freeze_var(&mut self, var: Var) -> anyhow::Result<()> {
+        unsafe { ffi::cminisatsimp_set_frozen(self.handle, var.to_ipasir(), true) };
+        Ok(())
+    }
+
+    fn melt_var(&mut self, var: Var) -> anyhow::Result<()> {
+        unsafe { ffi::cminisatsimp_set_frozen(self.handle, var.to_ipasir(), false) };
+        Ok(())
+    }
+
+    fn is_frozen(&mut self, var: Var) -> anyhow::Result<bool> {
+        Ok(unsafe { ffi::cminisatsimp_is_frozen(self.handle, var.to_ipasir()) } != 0)
+    }
+}
+
 impl LimitConflicts for Minisat {
-    fn limit_conflicts(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
+    fn limit_conflicts(&mut self, limit: Option<u32>) -> anyhow::Result<()> {
         self.set_limit(Limit::Conflicts(if let Some(limit) = limit {
             limit as i64
         } else {
@@ -267,7 +288,7 @@ impl LimitConflicts for Minisat {
 }
 
 impl LimitPropagations for Minisat {
-    fn limit_propagations(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
+    fn limit_propagations(&mut self, limit: Option<u32>) -> anyhow::Result<()> {
         self.set_limit(Limit::Propagations(if let Some(limit) = limit {
             limit as i64
         } else {
@@ -421,7 +442,8 @@ mod ffi {
         pub fn cminisatsimp_set_no_limit(solver: *mut MinisatHandle);
         pub fn cminisatsimp_interrupt(solver: *mut MinisatHandle);
         pub fn cminisatsimp_set_frozen(solver: *mut MinisatHandle, var: c_int, frozen: bool);
-        pub fn cminisatsimp_is_eliminated(solver: *mut MinisatHandle, var: c_int);
+        pub fn cminisatsimp_is_frozen(solver: *mut MinisatHandle, var: c_int) -> c_int;
+        pub fn cminisatsimp_is_eliminated(solver: *mut MinisatHandle, var: c_int) -> c_int;
         pub fn cminisatsimp_propagations(solver: *mut MinisatHandle) -> u64;
         pub fn cminisatsimp_decisions(solver: *mut MinisatHandle) -> u64;
         pub fn cminisatsimp_conflicts(solver: *mut MinisatHandle) -> u64;
diff --git a/rustsat/Cargo.toml b/rustsat/Cargo.toml
index d1183b53..95f254d1 100644
--- a/rustsat/Cargo.toml
+++ b/rustsat/Cargo.toml
@@ -16,14 +16,21 @@ build = "build.rs"
 [dependencies]
 nom = "7.1.1"
 bzip2 = { version = "0.4.4", optional = true }
-flate2 = { version = "1.0.25", optional = true, features = ["zlib-ng"], default-features = false }
+flate2 = { version = "1.0.25", optional = true, features = [
+  "zlib-ng",
+], default-features = false }
 xz2 = { version = "0.1.7", optional = true }
 rustc-hash = { version = "1.1.0", optional = true }
 cpu-time = "1.0.0"
 rand = { version = "0.8.5", optional = true }
 visibility = { version = "0.1.0" }
+anyhow = { version = "1.0.80" }
 thiserror = { version = "1.0.50" }
-pyo3 = { version = "0.20.0", optional = true, features = ["extension-module", "abi3", "abi3-py37"] }
+pyo3 = { version = "0.20.0", optional = true, features = [
+  "extension-module",
+  "abi3",
+  "abi3-py37",
+] }
 
 [build-dependencies]
 cbindgen = "0.26.0"
@@ -35,25 +42,16 @@ rustsat-minisat = { version = "0.2", path = "../minisat" }
 rustsat-tools = { version = "0.2", path = "../tools" }
 
 [features]
-default = [
-  "optimization",
-  "fxhash"
-]
+default = ["optimization", "fxhash"]
 internals = []
 fxhash = ["dep:rustc-hash"]
-ipasir = []
 optimization = []
 multiopt = ["optimization"]
 compression = ["dep:bzip2", "dep:flate2", "dep:xz2"]
 rand = ["dep:rand"]
 bench = []
 pyapi = ["dep:pyo3", "dep:pyo3-build-config"]
-all = [
-  "multiopt",
-  "compression",
-  "rand",
-  "fxhash",
-]
+all = ["multiopt", "compression", "rand", "fxhash"]
 
 [lib]
 crate-type = ["lib", "staticlib", "cdylib"]
diff --git a/rustsat/src/encodings/pb/dpw.rs b/rustsat/src/encodings/pb/dpw.rs
index 8c6e9beb..14e70099 100644
--- a/rustsat/src/encodings/pb/dpw.rs
+++ b/rustsat/src/encodings/pb/dpw.rs
@@ -129,7 +129,18 @@ impl BoundUpper for DynamicPolyWatchdog {
     fn enforce_ub(&self, ub: usize) -> Result<Vec<Lit>, Error> {
         match &self.structure {
             Some(structure) => enforce_ub(structure, ub, &self.db),
-            None => Ok(vec![]),
+            None => {
+                if self.weight_sum() <= ub {
+                    return Ok(vec![]);
+                }
+                if self.in_lits.len() > 1 {
+                    return Err(Error::NotEncoded);
+                }
+                debug_assert_eq!(self.in_lits.len(), 1);
+                let (l, w) = self.in_lits.iter().next().unwrap();
+                debug_assert!(*w > ub);
+                Ok(vec![-(*l)])
+            }
         }
     }
 
@@ -137,10 +148,13 @@ impl BoundUpper for DynamicPolyWatchdog {
         match &self.structure {
             Some(structure) => {
                 let output_weight = 1 << (structure.output_power());
+                if output_weight == 1 {
+                    return ub;
+                }
                 if ub < output_weight {
                     return ub;
                 }
-                ub / output_weight * output_weight - 1
+                (ub + 1) / output_weight * output_weight - 1
             }
             None => ub,
         }
@@ -158,7 +172,7 @@ impl BoundUpperIncremental for DynamicPolyWatchdog {
         R: RangeBounds<usize>,
     {
         let range = super::prepare_ub_range(self, range);
-        if range.is_empty() {
+        if range.is_empty() || self.in_lits.len() <= 1 {
             return;
         }
         let n_vars_before = var_manager.n_used();
@@ -656,6 +670,7 @@ mod tests {
         instances::{BasicVarManager, Cnf},
         lit,
         types::RsHashMap,
+        types::Var,
     };
 
     use super::DynamicPolyWatchdog;
@@ -668,13 +683,42 @@ mod tests {
         lits.insert(lit![2], 2);
         lits.insert(lit![3], 2);
         let mut dpw = DynamicPolyWatchdog::from(lits);
-        let mut var_manager = BasicVarManager::default();
+        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);
         assert_eq!(dpw.n_vars(), 9);
         assert_eq!(cnf.len(), 13);
     }
 
+    #[test]
+    fn single_lit() {
+        let mut lits = RsHashMap::default();
+        lits.insert(lit![0], 4);
+        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);
+        assert_eq!(dpw.n_vars(), 0);
+        assert_eq!(cnf.len(), 0);
+        debug_assert!(dpw.enforce_ub(4).unwrap().is_empty());
+        let assumps = dpw.enforce_ub(2).unwrap();
+        debug_assert_eq!(assumps.len(), 1);
+        debug_assert_eq!(assumps[0], -lit![0]);
+    }
+
+    #[test]
+    fn no_lit() {
+        let lits = RsHashMap::default();
+        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);
+        assert_eq!(dpw.n_vars(), 0);
+        assert_eq!(cnf.len(), 0);
+        debug_assert!(dpw.enforce_ub(4).unwrap().is_empty());
+        debug_assert!(dpw.enforce_ub(0).unwrap().is_empty());
+    }
+
     #[test]
     fn coarse_convergence() {
         let mut lits = RsHashMap::default();
@@ -685,10 +729,32 @@ 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);
-        for ub in 8..=23 {
+        dpw.encode_ub(0..23, &mut cnf, &mut var_manager);
+        for ub in 7..23 {
             let coarse_ub = dpw.coarse_ub(ub);
             debug_assert!(coarse_ub <= ub);
+            if ub % 8 == 7 {
+                debug_assert_eq!(coarse_ub, ub);
+            }
+            let assumps = dpw.enforce_ub(coarse_ub).unwrap();
+            debug_assert_eq!(assumps.len(), 1);
+        }
+    }
+
+    #[test]
+    fn coarse_convergence_unweighted() {
+        let mut lits = RsHashMap::default();
+        lits.insert(lit![0], 1);
+        lits.insert(lit![1], 1);
+        lits.insert(lit![2], 1);
+        lits.insert(lit![3], 1);
+        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);
+        for ub in 0..4 {
+            let coarse_ub = dpw.coarse_ub(ub);
+            debug_assert_eq!(coarse_ub, ub);
             let assumps = dpw.enforce_ub(coarse_ub).unwrap();
             debug_assert_eq!(assumps.len(), 1);
         }
diff --git a/rustsat/src/instances/fio.rs b/rustsat/src/instances/fio.rs
index ed2b8cf9..1fa11360 100644
--- a/rustsat/src/instances/fio.rs
+++ b/rustsat/src/instances/fio.rs
@@ -5,38 +5,15 @@
 //! directly.
 
 use std::{fs::File, io, path::Path};
-
 use thiserror::Error;
 
 pub mod dimacs;
-
 pub mod opb;
 
-/// Combined Parsing Errors
-#[derive(Error, Debug)]
-pub enum ParsingError {
-    /// IO Errors
-    #[error("IO error: {0}")]
-    IO(std::io::Error),
-    /// Dimacs Parsing Error
-    #[error("Dimacs error: {0}")]
-    Dimacs(dimacs::Error),
-    /// OPB Parsing Error
-    #[error("OPB error: {0}")]
-    Opb(opb::Error),
-}
-
-impl From<dimacs::Error> for ParsingError {
-    fn from(de: dimacs::Error) -> Self {
-        ParsingError::Dimacs(de)
-    }
-}
-
-impl From<opb::Error> for ParsingError {
-    fn from(oe: opb::Error) -> Self {
-        ParsingError::Opb(oe)
-    }
-}
+/// An error for when a requested objective does not exist
+#[derive(Error, Debug, PartialEq, Eq, Clone, Copy)]
+#[error("the file only has {0} objectives")]
+pub struct ObjNoExist(usize);
 
 /// Opens a reader for the file at Path.
 /// With feature `compression` supports bzip2 and gzip compression.
diff --git a/rustsat/src/instances/fio/dimacs.rs b/rustsat/src/instances/fio/dimacs.rs
index 81574a63..76e9e92e 100644
--- a/rustsat/src/instances/fio/dimacs.rs
+++ b/rustsat/src/instances/fio/dimacs.rs
@@ -14,12 +14,13 @@ use crate::{
     instances::{Cnf, ManageVars, SatInstance},
     types::{Clause, Lit, Var},
 };
+use anyhow::Context;
 use nom::{
     branch::alt,
     bytes::complete::tag,
     character::complete::{i32, line_ending, multispace0, multispace1, u64},
-    combinator::{all_consuming, map_res, recognize, success},
-    error::{Error as NomError, ErrorKind, ParseError},
+    combinator::{all_consuming, map, map_res, recognize, success},
+    error::{context, Error as NomError},
     multi::separated_list0,
     sequence::{pair, terminated, tuple},
     IResult,
@@ -44,8 +45,13 @@ type BodyContent<VM> = (SatInstance<VM>, Vec<Objective>);
 #[cfg(not(feature = "optimization"))]
 type BodyContent<VM> = SatInstance<VM>;
 
+/// An error for when an invalid p line is encountered
+#[derive(Error, Debug, PartialEq, Eq, Clone)]
+#[error("invalid p line '{0}'")]
+pub struct InvalidPLine(String);
+
 /// Parses a CNF instance from a reader (typically a (compressed) file)
-pub fn parse_cnf<R, VM>(reader: R) -> Result<SatInstance<VM>, Error>
+pub fn parse_cnf<R, VM>(reader: R) -> anyhow::Result<SatInstance<VM>>
 where
     R: Read,
     VM: ManageVars + Default,
@@ -65,17 +71,19 @@ where
 #[cfg(feature = "optimization")]
 /// Parses a WCNF instance (old or new format) from a reader (typically a
 /// (compressed) file). The objective with the index obj_idx is used.
-pub fn parse_wcnf_with_idx<R, VM>(reader: R, obj_idx: usize) -> Result<OptInstance<VM>, Error>
+pub fn parse_wcnf_with_idx<R, VM>(reader: R, obj_idx: usize) -> anyhow::Result<OptInstance<VM>>
 where
     R: Read,
     VM: ManageVars + Default,
 {
+    use super::ObjNoExist;
+
     let reader = BufReader::new(reader);
     let (constrs, mut objs) = parse_dimacs(reader)?;
     if objs.is_empty() {
         objs.push(Objective::default());
     } else if obj_idx >= objs.len() {
-        return Err(Error::ObjNoExist(objs.len()));
+        return Err(ObjNoExist(objs.len()).into());
     }
     Ok(OptInstance::compose(
         constrs,
@@ -85,7 +93,7 @@ where
 
 #[cfg(feature = "multiopt")]
 /// Parses a MCNF instance (old or new format) from a reader (typically a (compressed) file)
-pub fn parse_mcnf<R, VM>(reader: R) -> Result<MultiOptInstance<VM>, Error>
+pub fn parse_mcnf<R, VM>(reader: R) -> anyhow::Result<MultiOptInstance<VM>>
 where
     R: Read,
     VM: ManageVars + Default,
@@ -95,75 +103,6 @@ where
     Ok(MultiOptInstance::compose(constrs, objs))
 }
 
-/// Errors occuring within the DIMACS parsing module
-#[derive(Error, Debug)]
-pub enum Error {
-    /// Invalid literal in the file
-    #[error("invalid literal: {0}")]
-    Lit(String),
-    /// Invalid ending of a clause
-    #[error("invalid clause ending: {0}")]
-    ClauseEnding(String),
-    /// Invalid objective index
-    #[error("invalid objective index: {0}")]
-    ObjIdx(String),
-    /// Invalid weight
-    #[error("invalid weight: {0}")]
-    Weight(String),
-    /// A comment appeared in a clause
-    #[error("found comment in clause: {0}")]
-    CommentInClause(String),
-    /// The preamble never ended
-    #[error("preamble never ends")]
-    PreambleNoEnd,
-    /// P line value is too large to fit in a [`usize`]
-    #[error("value in p-line too large to fit usize: {0}")]
-    PValTooLarge(u64),
-    /// Invalid p line
-    #[error("invalid p-line: {0}")]
-    PLine(String),
-    /// The requested objective does not exist
-    #[error("the file only has {0} objectives")]
-    ObjNoExist(usize),
-    /// IO error reading file
-    #[error("IO error: {0}")]
-    IOError(io::Error),
-    /// Base error from nom parsing
-    #[error("nom error: {0} ({1:?})")]
-    NomError(String, ErrorKind),
-    /// Incomplete nom error
-    #[error("nom parser requested more data")]
-    NomIncomplete,
-}
-
-impl PartialEq for Error {
-    fn eq(&self, other: &Self) -> bool {
-        match (self, other) {
-            (Self::Lit(l0), Self::Lit(r0)) => l0 == r0,
-            (Self::ClauseEnding(l0), Self::ClauseEnding(r0)) => l0 == r0,
-            (Self::ObjIdx(l0), Self::ObjIdx(r0)) => l0 == r0,
-            (Self::Weight(l0), Self::Weight(r0)) => l0 == r0,
-            (Self::CommentInClause(l0), Self::CommentInClause(r0)) => l0 == r0,
-            (Self::ObjNoExist(l0), Self::ObjNoExist(r0)) => l0 == r0,
-            (Self::IOError(_), Self::IOError(_)) => true,
-            (Self::NomError(l0, l1), Self::NomError(r0, r1)) => l0 == r0 && l1 == r1,
-            _ => core::mem::discriminant(self) == core::mem::discriminant(other),
-        }
-    }
-}
-
-impl ParseError<&str> for Error {
-    fn from_error_kind(input: &str, kind: ErrorKind) -> Self {
-        Self::NomError(String::from(input), kind)
-    }
-
-    fn append(_: &str, _: ErrorKind, other: Self) -> Self {
-        // Other error always has precedence. This should prefer more meaningful
-        // errors than [`DimacsError::NomError`]
-        other
-    }
-}
-
 /// Internal type of possible preambles
 #[derive(PartialEq, Debug)]
 enum Preamble {
@@ -184,7 +123,7 @@ enum Preamble {
 }
 
 /// Top level parser
-fn parse_dimacs<R, VM>(reader: R) -> Result<BodyContent<VM>, Error>
+fn parse_dimacs<R, VM>(reader: R) -> anyhow::Result<BodyContent<VM>>
 where
     R: BufRead,
     VM: ManageVars + Default,
@@ -207,95 +146,73 @@ where
     Ok(content)
 }
 
-fn unwrap_dimacs_error(err: nom::Err<Error>) -> Error {
-    match err {
-        nom::Err::Incomplete(_) => Error::NomIncomplete,
-        nom::Err::Error(e) => e,
-        nom::Err::Failure(e) => e,
-    }
-}
-
 /// Parses preamble and determines type of instance/file format
-fn parse_preamble<R: BufRead>(mut reader: R) -> Result<(R, Preamble), Error> {
-    loop {
-        let mut buf = String::new();
-        match reader.read_line(&mut buf) {
-            Ok(len) => {
-                if len == 0 {
-                    #[cfg(feature = "optimization")]
-                    return Ok((
-                        reader,
-                        Preamble::NoPLine {
-                            first_line: String::from(""),
-                        },
-                    ));
-                    #[cfg(not(feature = "optimization"))]
-                    return Err(Error::PreambleNoEnd);
-                }
-            }
-            Err(ioe) => return Err(Error::IOError(ioe)),
-        };
+fn parse_preamble<R: BufRead>(mut reader: R) -> anyhow::Result<(R, Preamble)> {
+    let mut buf = String::new();
+    while reader.read_line(&mut buf)? > 0 {
         if buf.starts_with('c') || buf.trim().is_empty() {
+            buf.clear();
             continue;
         }
         if buf.starts_with('p') {
-            let (_, preamble) = parse_p_line(&buf).map_err(unwrap_dimacs_error)?;
+            let (_, preamble) = parse_p_line(&buf)
+                .map_err(|e| e.to_owned())
+                .with_context(|| format!("failed to parse p line '{}'", buf))?;
             return Ok((reader, preamble));
         }
-        #[cfg(feature = "optimization")]
-        return Ok((reader, Preamble::NoPLine { first_line: buf }));
-        #[cfg(not(feature = "optimization"))]
-        return Err(Error::PLine(buf));
+        break;
+    }
+    #[cfg(feature = "optimization")]
+    {
+        Ok((reader, Preamble::NoPLine { first_line: buf }))
+    }
+    #[cfg(not(feature = "optimization"))]
+    {
+        Err(InvalidPLine(buf).into())
     }
 }
 
 /// Main parser for CNF file
-fn parse_cnf_body<R, VM>(mut reader: R) -> Result<BodyContent<VM>, Error>
+fn parse_cnf_body<R, VM>(mut reader: R) -> anyhow::Result<BodyContent<VM>>
 where
     R: BufRead,
     VM: ManageVars + Default,
 {
     let mut inst = SatInstance::<VM>::new();
-    loop {
-        let mut buf = String::new();
-        match reader.read_line(&mut buf) {
-            Ok(len) => {
-                if len == 0 {
-                    #[cfg(feature = "optimization")]
-                    return Ok((inst, vec![]));
-                    #[cfg(not(feature = "optimization"))]
-                    return Ok(inst);
-                }
-            }
-            Err(ioe) => return Err(Error::IOError(ioe)),
-        };
-        let (_, opt_clause) = parse_cnf_line(&buf).map_err(unwrap_dimacs_error)?;
+    let mut buf = String::new();
+    while reader.read_line(&mut buf)? > 0 {
+        let (_, opt_clause) = parse_cnf_line(&buf)
+            .map_err(|e| e.to_owned())
+            .with_context(|| format!("failed to parse cnf line '{}'", buf))?;
         if let Some(clause) = opt_clause {
             inst.add_clause(clause)
         }
+        buf.clear();
+    }
+    #[cfg(feature = "optimization")]
+    {
+        Ok((inst, vec![]))
+    }
+    #[cfg(not(feature = "optimization"))]
+    {
+        Ok(inst)
     }
 }
 
 #[cfg(feature = "optimization")]
 /// Main parser for WCNF pre 22 (with p line)
-fn parse_wcnf_pre22_body<R, VM>(mut reader: R, top: usize) -> Result<BodyContent<VM>, Error>
+fn parse_wcnf_pre22_body<R, VM>(mut reader: R, top: usize) -> anyhow::Result<BodyContent<VM>>
 where
     R: BufRead,
     VM: ManageVars + Default,
 {
     let mut constrs = SatInstance::<VM>::new();
     let mut obj = Objective::new();
-    loop {
-        let mut buf = String::new();
-        match reader.read_line(&mut buf) {
-            Ok(len) => {
-                if len == 0 {
-                    return Ok((constrs, if obj.is_empty() { vec![] } else { vec![obj] }));
-                }
-            }
-            Err(ioe) => return Err(Error::IOError(ioe)),
-        };
-        let (_, opt_wclause) = parse_wcnf_pre22_line(&buf).map_err(unwrap_dimacs_error)?;
+    let mut buf = String::new();
+    while reader.read_line(&mut buf)? > 0 {
+        let (_, opt_wclause) = parse_wcnf_pre22_line(&buf)
+            .map_err(|e| e.to_owned())
+            .with_context(|| format!("failed to parse old wcnf line '{}'", buf))?;
         match opt_wclause {
             None => (),
             Some((w, clause)) => {
@@ -306,12 +223,14 @@ where
                 }
             }
         };
+        buf.clear();
     }
+    Ok((constrs, if obj.is_empty() { vec![] } else { vec![obj] }))
 }
 
 #[cfg(feature = "optimization")]
 /// Main parser for WCNF post 22 (without p line) and MCNF
-fn parse_no_pline_body<R, VM>(mut reader: R, first_line: &str) -> Result<BodyContent<VM>, Error>
+fn parse_no_pline_body<R, VM>(mut reader: R, first_line: &str) -> anyhow::Result<BodyContent<VM>>
 where
     R: BufRead,
     VM: ManageVars + Default,
@@ -320,7 +239,9 @@ where
     let mut objs = Vec::new();
     let mut buf = first_line.to_string();
     loop {
-        let (_, opt_wclause) = parse_mcnf_line(&buf).map_err(unwrap_dimacs_error)?;
+        let (_, opt_wclause) = parse_mcnf_line(&buf)
+            .map_err(|e| e.to_owned())
+            .with_context(|| format!("failed to parse new wcnf/mcnf line '{}'", buf))?;
         if let Some((opt_iw, clause)) = opt_wclause {
             match opt_iw {
                 Some((idx, w)) => {
@@ -333,74 +254,80 @@ where
             }
         };
         buf.clear();
-        match reader.read_line(&mut buf) {
-            Ok(len) => {
-                if len == 0 {
-                    return Ok((constrs, objs));
-                }
-            }
-            Err(ioe) => return Err(Error::IOError(ioe)),
-        };
+        let len = reader.read_line(&mut buf)?;
+        if len == 0 {
+            return Ok((constrs, objs));
+        }
     }
 }
 
 /// Parses p line and determine file format
-fn parse_p_line(input: &str) -> IResult<&str, Preamble, Error> {
-    let full_p_line = String::from(input);
-    let (input, _) = terminated::<_, _, _, NomError<_>, _, _>(tag("p"), multispace1)(input)
-        .map_err(|e| e.map(|_| Error::PLine(full_p_line.clone())))?;
-    let (input, id_token) = alt((
-        terminated::<_, _, _, NomError<_>, _, _>(tag("cnf"), multispace1),
-        #[cfg(feature = "optimization")]
-        terminated(tag("wcnf"), multispace1),
-    ))(input)
-    .map_err(|e| e.map(|_| Error::PLine(full_p_line.clone())))?;
+fn parse_p_line(input: &str) -> IResult<&str, Preamble> {
+    let (input, _) = context(
+        "p line does not start with 'p'",
+        terminated::<_, _, _, NomError<_>, _, _>(tag("p"), multispace1),
+    )(input)?;
+    let (input, id_token) = context(
+        "invalid id token in p line",
+        alt((
+            terminated::<_, _, _, NomError<_>, _, _>(tag("cnf"), multispace1),
+            #[cfg(feature = "optimization")]
+            terminated(tag("wcnf"), multispace1),
+        )),
+    )(input)?;
+    //.with_context(|| format!("invalid id token in '{}'", input))?;
     if id_token == "cnf" {
         // Is CNF file
-        let (input, (n_vars, _, n_clauses)) =
-            tuple::<_, _, NomError<_>, _>((u64, multispace1, u64))(input)
-                .map_err(|e| e.map(|_| Error::PLine(full_p_line)))?;
-        // Safe cast to usize
-        let n_vars = match usize::try_from(n_vars) {
-            Ok(v) => v,
-            Err(_) => return Err(nom::Err::Error(Error::PValTooLarge(n_vars))),
-        };
-        let n_clauses = match usize::try_from(n_clauses) {
-            Ok(v) => v,
-            Err(_) => return Err(nom::Err::Error(Error::PValTooLarge(n_clauses))),
-        };
+        let (input, (n_vars, _, n_clauses)) = context(
+            "failed to parse number of variables and clauses",
+            tuple::<_, _, NomError<_>, _>((
+                context(
+                    "number of vars does not fit usize",
+                    map_res(u64, usize::try_from),
+                ),
+                multispace1,
+                context(
+                    "number of clauses does not fit usize",
+                    map_res(u64, usize::try_from),
+                ),
+            )),
+        )(input)?;
         return Ok((input, Preamble::Cnf { n_vars, n_clauses }));
     }
     #[cfg(feature = "optimization")]
     if id_token == "wcnf" {
         // Is WCNF file
-        let (input, (n_vars, _, n_clauses, _, top)) =
-            tuple::<_, _, NomError<_>, _>((u64, multispace1, u64, multispace1, u64))(input)
-                .map_err(|e| e.map(|_| Error::PLine(full_p_line)))?;
-        // Safe cast to usize
-        let n_vars = match usize::try_from(n_vars) {
-            Ok(v) => v,
-            Err(_) => return Err(nom::Err::Error(Error::PValTooLarge(n_vars))),
-        };
-        let n_clauses = match usize::try_from(n_clauses) {
-            Ok(v) => v,
-            Err(_) => return Err(nom::Err::Error(Error::PValTooLarge(n_clauses))),
-        };
+        let (input, (n_vars, _, n_clauses, _, top)) = context(
+            "failed to parse number of variables, clauses, and top",
+            tuple::<_, _, NomError<_>, _>((
+                context(
+                    "number of vars does not fit usize",
+                    map_res(u64, usize::try_from),
+                ),
+                multispace1,
+                context(
+                    "number of clauses does not fit usize",
+                    map_res(u64, usize::try_from),
+                ),
+                multispace1,
+                context("top does not fit usize", map_res(u64, usize::try_from)),
+            )),
+        )(input)?;
         return Ok((
             input,
             Preamble::WcnfPre22 {
                 n_vars,
                 n_clauses,
-                top: top.try_into().unwrap(),
+                top,
             },
         ));
     }
-    Err(nom::Err::Error(Error::PLine(full_p_line)))
+    panic!("this should be impossible to reach")
 }
 
 /// Parses a CNF line, either a comment or a clause
-fn parse_cnf_line(input: &str) -> IResult<&str, Option<Clause>, Error> {
-    let (input, _) = multispace0(input)?;
+fn parse_cnf_line(input: &str) -> IResult<&str, Option<Clause>> {
+    let (input, _) = multispace0::<_, NomError<_>>(input)?;
     if input.trim().is_empty() {
         // Tolerate empty lines
         return Ok((input, None));
@@ -409,17 +336,16 @@ fn parse_cnf_line(input: &str) -> IResult<&str, Option<Clause>, Error> {
         Ok((input, _)) => Ok((input, None)),
         Err(_) => {
             // Line is not a comment
-            let (input, clause) =
-                terminated(separated_list0(multispace1, parse_lit), parse_clause_ending)(input)?;
-            Ok((input, Some(Clause::from_iter(clause))))
+            let (input, clause) = parse_clause(input)?;
+            Ok((input, Some(clause)))
         }
     }
 }
 
 #[cfg(feature = "optimization")]
 /// Parses a WCNF pre 22 line, either a comment or a clause
-fn parse_wcnf_pre22_line(input: &str) -> IResult<&str, Option<(usize, Clause)>, Error> {
-    let (input, _) = multispace0(input)?;
+fn parse_wcnf_pre22_line(input: &str) -> IResult<&str, Option<(usize, Clause)>> {
+    let (input, _) = multispace0::<_, NomError<_>>(input)?;
     if input.trim().is_empty() {
         // Tolerate empty lines
         return Ok((input, None));
@@ -428,12 +354,9 @@ fn parse_wcnf_pre22_line(input: &str) -> IResult<&str, Option<(usize, Clause)>,
         Ok((input, _)) => Ok((input, None)),
         Err(_) => {
             // Line is not a comment
-            let (input, (weight, opt_clause)) =
-                separated_pair(parse_weight, multispace1, parse_cnf_line)(input)?;
-            match opt_clause {
-                Some(clause) => Ok((input, Some((weight, clause)))),
-                None => Err(nom::Err::Error(Error::CommentInClause(String::from(input)))),
-            }
+            let (input, (weight, clause)) =
+                separated_pair(parse_weight, multispace1, parse_clause)(input)?;
+            Ok((input, Some((weight, clause))))
         }
     }
 }
@@ -445,8 +368,8 @@ type McnfDataLine = Option<(Option<(usize, usize)>, Clause)>;
 /// Parses a MCNF or WCNF post 22 line, either a comment or a clause with
 /// objective index. If a line does not explicitly specify an objective index,
 /// it is assumed to be 1. This enables for also parsing mcnf lines.
-fn parse_mcnf_line(input: &str) -> IResult<&str, McnfDataLine, Error> {
-    let (input, _) = multispace0(input)?;
+fn parse_mcnf_line(input: &str) -> IResult<&str, McnfDataLine> {
+    let (input, _) = multispace0::<_, NomError<_>>(input)?;
     if input.trim().is_empty() {
         // Tolerate empty lines
         return Ok((input, None));
@@ -456,45 +379,32 @@ fn parse_mcnf_line(input: &str) -> IResult<&str, McnfDataLine, Error> {
         Err(_) =>
         // Line is not a comment
         {
-            match terminated(tag::<&str, &str, NomError<&str>>("h"), multispace1)(input) {
+            match terminated(tag::<_, _, NomError<_>>("h"), multispace1)(input) {
                 Ok((input, _)) => {
                     // Hard clause
-                    let (input, opt_clause) = parse_cnf_line(input)?;
-                    match opt_clause {
-                        Some(clause) => Ok((input, Some((None, clause)))),
-                        None => Err(nom::Err::Error(Error::CommentInClause(String::from(input)))),
-                    }
+                    let (input, clause) = parse_clause(input)?;
+                    Ok((input, Some((None, clause))))
                 }
                 Err(_) => {
                     // Soft clause
-                    match tag::<&str, &str, NomError<&str>>("o")(input) {
+                    match tag::<_, _, NomError<_>>("o")(input) {
                         Ok((input, _)) => {
                             // MCNF soft (explicit obj index)
-                            let (input, (idx, _, weight, _, opt_clause)) =
+                            let (input, (idx, _, weight, _, clause)) =
                                 tuple((
                                     parse_idx,
                                     multispace1,
                                     parse_weight,
                                     multispace1,
-                                    parse_cnf_line,
+                                    parse_clause,
                                 ))(input)?;
-                            match opt_clause {
-                                Some(clause) => Ok((input, Some((Some((idx, weight)), clause)))),
-                                None => Err(nom::Err::Error(Error::CommentInClause(String::from(
-                                    input,
-                                )))),
-                            }
+                            Ok((input, Some((Some((idx, weight)), clause))))
                         }
                         Err(_) => {
                             // WCNF soft (implicit obj index of 1)
-                            let (input, (weight, opt_clause)) =
-                                separated_pair(parse_weight, multispace1, parse_cnf_line)(input)?;
-                            match opt_clause {
-                                Some(clause) => Ok((input, Some((Some((1, weight)), clause)))),
-                                None => Err(nom::Err::Error(Error::CommentInClause(String::from(
-                                    input,
-                                )))),
-                            }
+                            let (input, (weight, clause)) =
+                                separated_pair(parse_weight, multispace1, parse_clause)(input)?;
+                            Ok((input, Some((Some((1, weight)), clause))))
                         }
                     }
                 }
@@ -503,36 +413,50 @@ fn parse_mcnf_line(input: &str) -> IResult<&str, McnfDataLine, Error> {
     }
 }
 
+/// Nom-like parser for a clause
+fn parse_clause(input: &str) -> IResult<&str, Clause> {
+    context(
+        "failed to parse clause",
+        map(
+            terminated(separated_list0(multispace1, parse_lit), parse_clause_ending),
+            Clause::from_iter,
+        ),
+    )(input)
+}
+
 #[cfg(feature = "optimization")]
-/// Nuclear parser for weight value
-fn parse_weight(input: &str) -> IResult<&str, usize, Error> {
-    map_res(u64, |w| w.try_into())(input)
-        .map_err(|e| e.map(|e: NomError<&str>| Error::Weight(String::from(e.input))))
+/// Nom-like parser for weight value
+fn parse_weight(input: &str) -> IResult<&str, usize> {
+    context(
+        "weight does not fit usize",
+        map_res(context("expected number for weight", u64), |w| w.try_into()),
+    )(input)
 }
 
 #[cfg(feature = "optimization")]
-/// Nuclear parser for objective index
-fn parse_idx(input: &str) -> IResult<&str, usize, Error> {
-    map_res(u64, |w| {
-        if w == 0 {
-            return Err(());
-        }
-        w.try_into().map_err(|_| ())
-    })(input)
-    .map_err(|e| e.map(|e: NomError<&str>| Error::ObjIdx(String::from(e.input))))
+/// Nom-like parser for objective index
+fn parse_idx(input: &str) -> IResult<&str, usize> {
+    context(
+        "invalid objective index (either 0 or does not fit usize)",
+        map_res(context("expected number for objective index", u64), |w| {
+            if w == 0 {
+                return Err(());
+            }
+            w.try_into().map_err(|_| ())
+        }),
+    )(input)
 }
 
-/// Nuclear parser for literal
-fn parse_lit(input: &str) -> IResult<&str, Lit, Error> {
-    map_res(i32, Lit::from_ipasir)(input)
-        .map_err(|e| e.map(|e: NomError<&str>| Error::Lit(String::from(e.input))))
+/// Nom-like parser for literal
+fn parse_lit(input: &str) -> IResult<&str, Lit> {
+    context("invalid ipasir literal", map_res(i32, Lit::from_ipasir))(input)
 }
 
 /// Parses the end of a clause
 /// A '0' followed by a linebreak, as well as a '0' followed by
 /// whitespace or only a linebreak are treated as valid clause endings.
 /// This is more lean than the file format spec.
-fn parse_clause_ending(input: &str) -> IResult<&str, &str, Error> {
+fn parse_clause_ending(input: &str) -> IResult<&str, &str> {
     recognize(pair(
         multispace0,
         alt((
@@ -543,7 +467,6 @@ fn parse_clause_ending(input: &str) -> IResult<&str, &str, Error> {
             recognize(line_ending),
         )),
     ))(input)
-    .map_err(|e| e.map(|e: NomError<&str>| Error::ClauseEnding(String::from(e.input))))
 }
 
 /// Writes a CNF to a DIMACS CNF file
@@ -731,13 +654,14 @@ fn write_clause<W: Write>(writer: &mut W, clause: Clause) -> Result<(), io::Erro
 mod tests {
     use super::{
         parse_clause_ending, parse_cnf_body, parse_cnf_line, parse_dimacs, parse_lit, parse_p_line,
-        parse_preamble, write_cnf_annotated, Error, Preamble,
+        parse_preamble, write_cnf_annotated, Preamble,
     };
     use crate::{
         clause,
         instances::{Cnf, SatInstance},
         ipasir_lit, var,
     };
+    use nom::error::Error as NomError;
     use std::io::{Cursor, Seek};
 
     #[cfg(feature = "optimization")]
@@ -759,22 +683,14 @@ mod tests {
     #[cfg(feature = "optimization")]
     #[test]
     fn parse_idx_fail() {
-        assert_eq!(
-            parse_idx("0 "),
-            Err(nom::Err::Error(Error::ObjIdx(String::from("0 "))))
-        );
-        assert_eq!(
-            parse_idx("-15 "),
-            Err(nom::Err::Error(Error::ObjIdx(String::from("-15 "))))
-        );
-        assert_eq!(
-            parse_idx("abc "),
-            Err(nom::Err::Error(Error::ObjIdx(String::from("abc "))))
-        );
-        assert_eq!(
-            parse_idx(" abc "),
-            Err(nom::Err::Error(Error::ObjIdx(String::from(" abc "))))
-        );
+        assert!(parse_idx("0 ")
+            .is_err_and(|e| matches!(e, nom::Err::Error(NomError { input: "0 ", .. }))));
+        assert!(parse_idx("-15 ")
+            .is_err_and(|e| matches!(e, nom::Err::Error(NomError { input: "-15 ", .. }))));
+        assert!(parse_idx("abc ")
+            .is_err_and(|e| matches!(e, nom::Err::Error(NomError { input: "abc ", .. }))));
+        assert!(parse_idx(" abc ")
+            .is_err_and(|e| matches!(e, nom::Err::Error(NomError { input: " abc ", .. }))));
     }
 
     #[cfg(feature = "optimization")]
@@ -788,18 +704,12 @@ mod tests {
     #[cfg(feature = "optimization")]
     #[test]
     fn parse_weight_fail() {
-        assert_eq!(
-            parse_weight("-2 "),
-            Err(nom::Err::Error(Error::Weight(String::from("-2 "))))
-        );
-        assert_eq!(
-            parse_weight("abc "),
-            Err(nom::Err::Error(Error::Weight(String::from("abc "))))
-        );
-        assert_eq!(
-            parse_weight(" abc "),
-            Err(nom::Err::Error(Error::Weight(String::from(" abc "))))
-        );
+        assert!(parse_weight("-2 ")
+            .is_err_and(|e| matches!(e, nom::Err::Error(NomError { input: "-2 ", .. }))));
+        assert!(parse_weight("abc ")
+            .is_err_and(|e| matches!(e, nom::Err::Error(NomError { input: "abc ", .. }))));
+        assert!(parse_weight(" abc ")
+            .is_err_and(|e| matches!(e, nom::Err::Error(NomError { input: " abc ", .. }))));
     }
 
     #[test]
@@ -812,14 +722,10 @@ mod tests {
 
     #[test]
     fn parse_lit_fail() {
-        assert_eq!(
-            parse_lit("abc "),
-            Err(nom::Err::Error(Error::Lit(String::from("abc "))))
-        );
-        assert_eq!(
-            parse_lit(" abc "),
-            Err(nom::Err::Error(Error::Lit(String::from(" abc "))))
-        );
+        assert!(parse_lit("abc ")
+            .is_err_and(|e| matches!(e, nom::Err::Error(NomError { input: "abc ", .. }))));
+        assert!(parse_lit(" abc ")
+            .is_err_and(|e| matches!(e, nom::Err::Error(NomError { input: " abc ", .. }))));
     }
 
     #[test]
@@ -850,24 +756,32 @@ mod tests {
 
     #[test]
     fn parse_p_line_fail() {
-        assert_eq!(
-            parse_p_line("a cnf 23 42"),
-            Err(nom::Err::Error(Error::PLine(String::from("a cnf 23 42"))))
-        );
-        assert_eq!(
-            parse_p_line("p abc 23 42 52"),
-            Err(nom::Err::Error(Error::PLine(String::from(
-                "p abc 23 42 52"
-            ))))
-        );
-        assert_eq!(
-            parse_p_line("p cnf ab"),
-            Err(nom::Err::Error(Error::PLine(String::from("p cnf ab"))))
-        );
-        assert_eq!(
-            parse_p_line("p wcnf ab"),
-            Err(nom::Err::Error(Error::PLine(String::from("p wcnf ab"))))
-        );
+        assert!(parse_p_line("a cnf 23 42").is_err_and(|e| matches!(
+            e,
+            nom::Err::Error(NomError {
+                input: "a cnf 23 42",
+                ..
+            })
+        )));
+        assert!(parse_p_line("p abc 23 42 52").is_err_and(|e| matches!(
+            e,
+            nom::Err::Error(NomError {
+                input: "abc 23 42 52",
+                ..
+            })
+        )));
+        assert!(parse_p_line("p cnf ab")
+            .is_err_and(|e| matches!(e, nom::Err::Error(NomError { input: "ab", .. }))));
+        assert!(parse_p_line("p wcnf ab")
+            .is_err_and(|e| matches!(e, nom::Err::Error(NomError { input: "ab", .. }))));
+        #[cfg(not(feature = "optimization"))]
+        assert!(parse_p_line("p wcnf 23 42 52").is_err_and(|e| matches!(
+            e,
+            nom::Err::Error(NomError {
+                input: "wcnf 23 42 52",
+                ..
+            })
+        )));
     }
 
     #[test]
@@ -880,14 +794,10 @@ mod tests {
 
     #[test]
     fn parse_clause_ending_fail() {
-        assert_eq!(
-            parse_clause_ending("test"),
-            Err(nom::Err::Error(Error::ClauseEnding(String::from("test"))))
-        );
-        assert_eq!(
-            parse_clause_ending("0test"),
-            Err(nom::Err::Error(Error::ClauseEnding(String::from("0test"))))
-        );
+        assert!(parse_clause_ending("test")
+            .is_err_and(|e| matches!(e, nom::Err::Error(NomError { input: "test", .. }))));
+        assert!(parse_clause_ending("0test")
+            .is_err_and(|e| matches!(e, nom::Err::Error(NomError { input: "0test", .. }))));
     }
 
     #[test]
@@ -912,12 +822,13 @@ mod tests {
 
     #[test]
     fn parse_cnf_line_fail() {
-        assert_eq!(
-            parse_cnf_line("42 34 a -16 0"),
-            Err(nom::Err::Error(Error::ClauseEnding(String::from(
-                "a -16 0"
-            ))))
-        );
+        assert!(parse_cnf_line("42 34 a -16 0").is_err_and(|e| matches!(
+            e,
+            nom::Err::Error(NomError {
+                input: "a -16 0",
+                ..
+            })
+        )));
     }
 
     #[cfg(feature = "optimization")]
diff --git a/rustsat/src/instances/fio/opb.rs b/rustsat/src/instances/fio/opb.rs
index 1cac1a8e..8c1d941e 100644
--- a/rustsat/src/instances/fio/opb.rs
+++ b/rustsat/src/instances/fio/opb.rs
@@ -15,13 +15,14 @@ use crate::{
         Clause, Lit, Var,
     },
 };
+use anyhow::Context;
 use nom::{
     branch::alt,
     bytes::complete::tag,
     character::complete::{anychar, i64, line_ending, space0, space1, u64},
-    combinator::{eof, map_res, recognize},
+    combinator::{cut, eof, map, map_res, recognize},
     error::Error as NomError,
-    multi::{many0, many_till},
+    multi::{many0, many1, many_till},
     sequence::{pair, tuple},
     IResult,
 };
@@ -29,7 +30,6 @@ use std::{
     io::{self, BufRead, BufReader, Read, Write},
     num::TryFromIntError,
 };
-use thiserror::Error;
 
 #[cfg(feature = "multiopt")]
 use crate::instances::MultiOptInstance;
@@ -38,20 +38,6 @@ use crate::instances::{Objective, OptInstance};
 #[cfg(feature = "optimization")]
 use crate::types::WLitIter;
 
-/// Errors occuring within the OPB parsing module
-#[derive(Error, Debug, PartialEq, Eq)]
-pub enum Error {
-    /// The requested objective does not exist
-    #[error("no matching objective found in file")]
-    ObjectiveNotFound,
-    /// Encountered an unexpected line in the OPB file
-    #[error("invalid OPB line: {0}")]
-    InvalidLine(String),
-    /// Error while reading input data
-    #[error("IO error")]
-    IOError,
-}
-
 /// Options for reading and writing OPB files
 /// Possible relational operators
 #[derive(Debug, PartialEq, Eq, Clone, Copy)]
@@ -104,7 +90,7 @@ enum OpbData {
 }
 
 /// Parses the constraints from an OPB file as a [`SatInstance`]
-pub fn parse_sat<R, VM>(reader: R, opts: Options) -> Result<SatInstance<VM>, Error>
+pub fn parse_sat<R, VM>(reader: R, opts: Options) -> anyhow::Result<SatInstance<VM>>
 where
     R: Read,
     VM: ManageVars + Default,
@@ -126,11 +112,13 @@ pub fn parse_opt_with_idx<R, VM>(
     reader: R,
     obj_idx: usize,
     opts: Options,
-) -> Result<OptInstance<VM>, Error>
+) -> anyhow::Result<OptInstance<VM>>
 where
     R: Read,
     VM: ManageVars + Default,
 {
+    use super::ObjNoExist;
+
     let data = parse_opb_data(reader, opts)?;
     let mut sat_inst = SatInstance::<VM>::new();
     let mut obj_cnt = 0;
@@ -150,7 +138,7 @@ where
         }
     });
     if obj_cnt <= obj_idx {
-        Err(Error::ObjectiveNotFound)
+        Err(ObjNoExist(obj_cnt).into())
     } else {
         Ok(OptInstance::compose(sat_inst, obj))
     }
@@ -159,7 +147,7 @@ where
 #[cfg(feature = "multiopt")]
 /// Parses an OPB file as an [`MultiOptInstance`] using the objective with the given
 /// index (starting from 0).
-pub fn parse_multi_opt<R, VM>(reader: R, opts: Options) -> Result<MultiOptInstance<VM>, Error>
+pub fn parse_multi_opt<R, VM>(reader: R, opts: Options) -> anyhow::Result<MultiOptInstance<VM>>
 where
     R: Read,
     VM: ManageVars + Default,
@@ -176,27 +164,25 @@ where
 }
 
 /// Parses all OPB data of a reader
-fn parse_opb_data<R: Read>(reader: R, opts: Options) -> Result<Vec<OpbData>, Error> {
+fn parse_opb_data<R: Read>(reader: R, opts: Options) -> anyhow::Result<Vec<OpbData>> {
     let mut reader = BufReader::new(reader);
     let mut buf = String::new();
     let mut data = vec![];
-    while let Ok(len) = reader.read_line(&mut buf) {
-        if len == 0 {
-            return Ok(data);
-        }
-        match many0(|i| opb_data(i, opts))(&buf) {
-            Ok((rem, new_data)) => {
-                if !rem.is_empty() {
-                    return Err(Error::InvalidLine(buf.clone()));
-                } else {
-                    data.extend(new_data)
-                }
-            }
-            Err(_) => return Err(Error::InvalidLine(buf.clone())),
+    // TODO: consider not necessarily reading a full line
+    while reader.read_line(&mut buf)? > 0 {
+        let (rem, new_data) = many0(|i| opb_data(i, opts))(&buf)
+            .map_err(|e| e.to_owned())
+            .with_context(|| format!("failed to parse opb line '{}'", buf))?;
+        data.extend(new_data);
+        if !rem.is_empty() {
+            // continue with remainder, this allows for line breaks within constraints etc
+            // TODO: to work, this requires the opb_ending function to be adapted
+            buf = String::from(rem);
+        } else {
+            buf.clear();
         }
-        buf.clear();
     }
-    Err(Error::IOError)
+    Ok(data)
 }
 
 /// Matches an OPB comment
@@ -255,19 +241,26 @@ fn weight(input: &str) -> IResult<&str, isize> {
 
 /// Parses an OPB weighted term
 fn weighted_literal(input: &str, opts: Options) -> IResult<&str, (Lit, isize)> {
-    map_res(
-        tuple((weight, space1, |i| literal(i, opts), space0)),
-        |(w, _, l, _)| Ok::<_, ()>((l, w)),
+    map(
+        tuple((weight, cut(space1), cut(|i| literal(i, opts)), space0)),
+        |(w, _, l, _)| (l, w),
     )(input)
 }
 
 /// Parses an OPB sum
 fn weighted_lit_sum(input: &str, opts: Options) -> IResult<&str, Vec<(Lit, isize)>> {
+    many1(|i| weighted_literal(i, opts))(input)
+}
+
+#[cfg(feature = "optimization")]
+/// Parses a (potentially empty) OPB sum
+fn weighted_lit_sum0(input: &str, opts: Options) -> IResult<&str, Vec<(Lit, isize)>> {
     many0(|i| weighted_literal(i, opts))(input)
 }
 
 /// Leniently parses OPB constraint or objective ending as ';' or a line ending
 fn opb_ending(input: &str) -> IResult<&str, &str> {
+    // TODO: potentially simplify with `cut`?
     recognize(pair(
         space0,
         alt((
@@ -289,10 +282,10 @@ fn constraint(input: &str, opts: Options) -> IResult<&str, PBConstraint> {
     map_res(
         tuple((
             |i| weighted_lit_sum(i, opts),
-            operator,
+            cut(operator),
             space0,
-            weight,
-            opb_ending,
+            cut(weight),
+            cut(opb_ending),
         )),
         |(wls, op, _, b, _)| {
             let lits = wls.into_iter();
@@ -314,8 +307,8 @@ fn objective(input: &str, opts: Options) -> IResult<&str, Objective> {
         tuple((
             tag("min:"),
             space0,
-            |i| weighted_lit_sum(i, opts),
-            opb_ending,
+            |i| weighted_lit_sum0(i, opts),
+            cut(opb_ending),
         )),
         |(_, _, wsl, _)| {
             let mut obj = Objective::new();
@@ -342,17 +335,14 @@ fn opb_data(input: &str, opts: Options) -> IResult<&str, OpbData> {
     // remove leading spaces
     let (input, _) = space0(input)?;
     alt((
-        map_res(comment, |cmt| Ok::<_, ()>(OpbData::Cmt(String::from(cmt)))),
-        map_res(
-            |i| constraint(i, opts),
-            |constr| Ok::<_, ()>(OpbData::Constr(constr)),
-        ),
+        map(comment, |cmt| OpbData::Cmt(String::from(cmt))),
+        map(|i| constraint(i, opts), OpbData::Constr),
         #[cfg(feature = "optimization")]
-        map_res(|i| objective(i, opts), |obj| Ok::<_, ()>(OpbData::Obj(obj))),
+        map(|i| objective(i, opts), OpbData::Obj),
         #[cfg(not(feature = "optimization"))]
-        map_res(
+        map(
             |i| objective(i, opts),
-            |obj| Ok::<_, ()>(OpbData::Obj(String::from(obj))),
+            |obj| OpbData::Obj(String::from(obj)),
         ),
     ))(input)
 }
@@ -703,7 +693,7 @@ mod test {
     use nom::error::{Error as NomError, ErrorKind};
 
     #[cfg(feature = "optimization")]
-    use super::{opb_data, parse_opb_data, Error, OpbData};
+    use super::{opb_data, parse_opb_data, OpbData};
     #[cfg(feature = "optimization")]
     use crate::instances::Objective;
     #[cfg(feature = "optimization")]
@@ -851,7 +841,7 @@ mod test {
         }
         match objective("min: x0;", Options::default()) {
             Ok(_) => panic!(),
-            Err(err) => assert_eq!(err, nom::Err::Error(NomError::new("x0;", ErrorKind::Eof))),
+            Err(err) => assert_eq!(err, nom::Err::Failure(NomError::new("x0;", ErrorKind::Eof))),
         }
         match objective("min:;", Options::default()) {
             Ok((rest, obj)) => {
@@ -885,6 +875,7 @@ mod test {
             opb_data("3 x1 -2 ~x2 <= 4;\n", Options::default()),
             Ok(("", OpbData::Constr(should_be_constr)))
         );
+        assert!(opb_data("", Options::default()).is_err_and(|e| matches!(e, nom::Err::Error(_))));
         #[cfg(feature = "optimization")]
         {
             let mut obj = Objective::new();
@@ -896,7 +887,7 @@ mod test {
             );
             assert_eq!(
                 opb_data("min: x1;", Options::default()),
-                Err(nom::Err::Error(NomError::new("x1;", ErrorKind::Eof)))
+                Err(nom::Err::Failure(NomError::new("x1;", ErrorKind::Eof)))
             );
         }
     }
@@ -912,12 +903,10 @@ mod test {
                 assert_eq!(data.len(), 3);
                 assert_eq!(data[0], OpbData::Cmt(String::from("* test\n")));
                 if let OpbData::Constr(_) = data[1] {
-                    ()
                 } else {
                     panic!()
                 }
                 if let OpbData::Obj(_) = data[2] {
-                    ()
                 } else {
                     panic!()
                 }
@@ -927,10 +916,7 @@ mod test {
         let data = "* test\n5 x1 -3 x2 >= 4;\nmin: x1;";
         let reader = Cursor::new(data);
         let reader = BufReader::new(reader);
-        assert_eq!(
-            parse_opb_data(reader, Options::default()),
-            Err(Error::InvalidLine(String::from("min: x1;")))
-        );
+        assert!(parse_opb_data(reader, Options::default()).is_err());
     }
 
     #[test]
diff --git a/rustsat/src/instances/multiopt.rs b/rustsat/src/instances/multiopt.rs
index 243d51ff..41ca4a00 100644
--- a/rustsat/src/instances/multiopt.rs
+++ b/rustsat/src/instances/multiopt.rs
@@ -275,17 +275,15 @@ impl<VM: ManageVars + Default> MultiOptInstance<VM> {
     /// positive number preceded by an 'o', indicating what objective this soft
     /// clause belongs to. After that, the format is identical to a soft clause
     /// in a WCNF file.
-    pub fn from_dimacs<R: io::Read>(reader: R) -> Result<Self, fio::ParsingError> {
-        Ok(fio::dimacs::parse_mcnf(reader)?)
+    pub fn from_dimacs<R: io::Read>(reader: R) -> anyhow::Result<Self> {
+        fio::dimacs::parse_mcnf(reader)
     }
 
     /// Parses a DIMACS instance from a file path. For more details see
     /// [`OptInstance::from_dimacs`](super::OptInstance::from_dimacs).
-    pub fn from_dimacs_path<P: AsRef<Path>>(path: P) -> Result<Self, fio::ParsingError> {
-        match fio::open_compressed_uncompressed_read(path) {
-            Err(why) => Err(fio::ParsingError::IO(why)),
-            Ok(reader) => MultiOptInstance::from_dimacs(reader),
-        }
+    pub fn from_dimacs_path<P: AsRef<Path>>(path: P) -> anyhow::Result<Self> {
+        let reader = fio::open_compressed_uncompressed_read(path)?;
+        Self::from_dimacs(reader)
     }
 
     /// Parses an OPB instance from a reader object.
@@ -296,24 +294,16 @@ impl<VM: ManageVars + Default> MultiOptInstance<VM> {
     /// pseudo-boolean optimization instances with multiple objectives defined.
     /// For details on the file format see
     /// [here](https://www.cril.univ-artois.fr/PB12/format.pdf).
-    pub fn from_opb<R: io::Read>(
-        reader: R,
-        opts: fio::opb::Options,
-    ) -> Result<Self, fio::ParsingError> {
-        Ok(fio::opb::parse_multi_opt(reader, opts)?)
+    pub fn from_opb<R: io::Read>(reader: R, opts: fio::opb::Options) -> anyhow::Result<Self> {
+        fio::opb::parse_multi_opt(reader, opts)
     }
 
     /// Parses an OPB instance from a file path. For more details see
     /// [`MultiOptInstance::from_opb`]. With feature `compression` supports
     /// bzip2 and gzip compression, detected by the file extension.
-    pub fn from_opb_path<P: AsRef<Path>>(
-        path: P,
-        opts: fio::opb::Options,
-    ) -> Result<Self, fio::ParsingError> {
-        match fio::open_compressed_uncompressed_read(path) {
-            Err(why) => Err(fio::ParsingError::IO(why)),
-            Ok(reader) => MultiOptInstance::from_opb(reader, opts),
-        }
+    pub fn from_opb_path<P: AsRef<Path>>(path: P, opts: fio::opb::Options) -> anyhow::Result<Self> {
+        let reader = fio::open_compressed_uncompressed_read(path)?;
+        Self::from_opb(reader, opts)
     }
 }
 
diff --git a/rustsat/src/instances/opt.rs b/rustsat/src/instances/opt.rs
index 5c302672..6bfb2608 100644
--- a/rustsat/src/instances/opt.rs
+++ b/rustsat/src/instances/opt.rs
@@ -1045,28 +1045,23 @@ impl<VM: ManageVars + Default> OptInstance<VM> {
     ///
     /// If a DIMACS MCNF file is passed to this function, all objectives but the
     /// first are ignored.
-    pub fn from_dimacs<R: io::Read>(reader: R) -> Result<Self, fio::ParsingError> {
+    pub fn from_dimacs<R: io::Read>(reader: R) -> anyhow::Result<Self> {
         Self::from_dimacs_with_idx(reader, 0)
     }
 
     /// Parses a DIMACS instance from a reader object, selecting the objective
     /// with index `obj_idx` if multiple are available. The index starts at 0.
     /// For more details see [`OptInstance::from_dimacs`].
-    pub fn from_dimacs_with_idx<R: io::Read>(
-        reader: R,
-        obj_idx: usize,
-    ) -> Result<Self, fio::ParsingError> {
-        Ok(fio::dimacs::parse_wcnf_with_idx(reader, obj_idx)?)
+    pub fn from_dimacs_with_idx<R: io::Read>(reader: R, obj_idx: usize) -> anyhow::Result<Self> {
+        fio::dimacs::parse_wcnf_with_idx(reader, obj_idx)
     }
 
     /// Parses a DIMACS instance from a file path. For more details see
     /// [`OptInstance::from_dimacs`]. With feature `compression` supports
     /// bzip2 and gzip compression, detected by the file extension.
-    pub fn from_dimacs_path<P: AsRef<Path>>(path: P) -> Result<Self, fio::ParsingError> {
-        match fio::open_compressed_uncompressed_read(path) {
-            Err(why) => Err(fio::ParsingError::IO(why)),
-            Ok(reader) => OptInstance::from_dimacs(reader),
-        }
+    pub fn from_dimacs_path<P: AsRef<Path>>(path: P) -> anyhow::Result<Self> {
+        let reader = fio::open_compressed_uncompressed_read(path)?;
+        Self::from_dimacs(reader)
     }
 
     /// Parses a DIMACS instance from a file path. For more details see
@@ -1075,11 +1070,9 @@ impl<VM: ManageVars + Default> OptInstance<VM> {
     pub fn from_dimacs_path_with_idx<P: AsRef<Path>>(
         path: P,
         obj_idx: usize,
-    ) -> Result<Self, fio::ParsingError> {
-        match fio::open_compressed_uncompressed_read(path) {
-            Err(why) => Err(fio::ParsingError::IO(why)),
-            Ok(reader) => OptInstance::from_dimacs_with_idx(reader, obj_idx),
-        }
+    ) -> anyhow::Result<Self> {
+        let reader = fio::open_compressed_uncompressed_read(path)?;
+        Self::from_dimacs_with_idx(reader, obj_idx)
     }
 
     /// Parses an OPB instance from a reader object.
@@ -1089,11 +1082,8 @@ impl<VM: ManageVars + Default> OptInstance<VM> {
     /// The file format expected by this parser is the OPB format for
     /// pseudo-boolean optimization instances. For details on the file format
     /// see [here](https://www.cril.univ-artois.fr/PB12/format.pdf).
-    pub fn from_opb<R: io::Read>(
-        reader: R,
-        opts: fio::opb::Options,
-    ) -> Result<Self, fio::ParsingError> {
-        OptInstance::from_opb_with_idx(reader, 0, opts)
+    pub fn from_opb<R: io::Read>(reader: R, opts: fio::opb::Options) -> anyhow::Result<Self> {
+        Self::from_opb_with_idx(reader, 0, opts)
     }
 
     /// Parses an OPB instance from a reader object, selecting the objective
@@ -1103,21 +1093,16 @@ impl<VM: ManageVars + Default> OptInstance<VM> {
         reader: R,
         obj_idx: usize,
         opts: fio::opb::Options,
-    ) -> Result<Self, fio::ParsingError> {
-        Ok(fio::opb::parse_opt_with_idx(reader, obj_idx, opts)?)
+    ) -> anyhow::Result<Self> {
+        fio::opb::parse_opt_with_idx(reader, obj_idx, opts)
     }
 
     /// Parses an OPB instance from a file path. For more details see
     /// [`OptInstance::from_opb`]. With feature `compression` supports
     /// bzip2 and gzip compression, detected by the file extension.
-    pub fn from_opb_path<P: AsRef<Path>>(
-        path: P,
-        opts: fio::opb::Options,
-    ) -> Result<Self, fio::ParsingError> {
-        match fio::open_compressed_uncompressed_read(path) {
-            Err(why) => Err(fio::ParsingError::IO(why)),
-            Ok(reader) => OptInstance::from_opb(reader, opts),
-        }
+    pub fn from_opb_path<P: AsRef<Path>>(path: P, opts: fio::opb::Options) -> anyhow::Result<Self> {
+        let reader = fio::open_compressed_uncompressed_read(path)?;
+        Self::from_opb(reader, opts)
     }
 
     /// Parses an OPB instance from a file path, selecting the objective with
@@ -1129,11 +1114,9 @@ impl<VM: ManageVars + Default> OptInstance<VM> {
         path: P,
         obj_idx: usize,
         opts: fio::opb::Options,
-    ) -> Result<Self, fio::ParsingError> {
-        match fio::open_compressed_uncompressed_read(path) {
-            Err(why) => Err(fio::ParsingError::IO(why)),
-            Ok(reader) => OptInstance::from_opb_with_idx(reader, obj_idx, opts),
-        }
+    ) -> anyhow::Result<Self> {
+        let reader = fio::open_compressed_uncompressed_read(path)?;
+        Self::from_opb_with_idx(reader, obj_idx, opts)
     }
 }
 
diff --git a/rustsat/src/instances/sat.rs b/rustsat/src/instances/sat.rs
index 4d5a0733..244930aa 100644
--- a/rustsat/src/instances/sat.rs
+++ b/rustsat/src/instances/sat.rs
@@ -14,6 +14,7 @@ use crate::{
 
 #[cfg(feature = "pyapi")]
 use crate::pyapi::{SingleOrList, SliceOrInt};
+use anyhow::Context;
 #[cfg(feature = "pyapi")]
 use pyo3::{
     exceptions::{PyIndexError, PyRuntimeError},
@@ -881,18 +882,17 @@ impl<VM: ManageVars + Default> SatInstance<VM> {
     ///
     /// If a DIMACS WCNF or MCNF file is parsed with this method, the objectives
     /// are ignored and only the constraints returned.
-    pub fn from_dimacs<R: io::Read>(reader: R) -> Result<Self, fio::ParsingError> {
-        Ok(fio::dimacs::parse_cnf(reader)?)
+    pub fn from_dimacs<R: io::Read>(reader: R) -> anyhow::Result<Self> {
+        fio::dimacs::parse_cnf(reader)
     }
 
     /// Parses a DIMACS instance from a file path. For more details see
     /// [`SatInstance::from_dimacs`]. With feature `compression` supports
     /// bzip2 and gzip compression, detected by the file extension.
-    pub fn from_dimacs_path<P: AsRef<Path>>(path: P) -> Result<Self, fio::ParsingError> {
-        match fio::open_compressed_uncompressed_read(path) {
-            Err(why) => Err(fio::ParsingError::IO(why)),
-            Ok(reader) => SatInstance::from_dimacs(reader),
-        }
+    pub fn from_dimacs_path<P: AsRef<Path>>(path: P) -> anyhow::Result<Self> {
+        let reader =
+            fio::open_compressed_uncompressed_read(path).context("failed to open reader")?;
+        SatInstance::from_dimacs(reader)
     }
 
     /// Parses an OPB instance from a reader object.
@@ -902,24 +902,17 @@ impl<VM: ManageVars + Default> SatInstance<VM> {
     /// The file format expected by this parser is the OPB format for
     /// pseudo-boolean satisfaction instances. For details on the file format
     /// see [here](https://www.cril.univ-artois.fr/PB12/format.pdf).
-    pub fn from_opb<R: io::Read>(
-        reader: R,
-        opts: fio::opb::Options,
-    ) -> Result<Self, fio::ParsingError> {
-        Ok(fio::opb::parse_sat(reader, opts)?)
+    pub fn from_opb<R: io::Read>(reader: R, opts: fio::opb::Options) -> anyhow::Result<Self> {
+        fio::opb::parse_sat(reader, opts)
     }
 
     /// Parses an OPB instance from a file path. For more details see
     /// [`SatInstance::from_opb`]. With feature `compression` supports
     /// bzip2 and gzip compression, detected by the file extension.
-    pub fn from_opb_path<P: AsRef<Path>>(
-        path: P,
-        opts: fio::opb::Options,
-    ) -> Result<Self, fio::ParsingError> {
-        match fio::open_compressed_uncompressed_read(path) {
-            Err(why) => Err(fio::ParsingError::IO(why)),
-            Ok(reader) => SatInstance::from_opb(reader, opts),
-        }
+    pub fn from_opb_path<P: AsRef<Path>>(path: P, opts: fio::opb::Options) -> anyhow::Result<Self> {
+        let reader =
+            fio::open_compressed_uncompressed_read(path).context("failed to open reader")?;
+        SatInstance::from_opb(reader, opts)
     }
 }
 
diff --git a/rustsat/src/lib.rs b/rustsat/src/lib.rs
index debd7540..71d22936 100644
--- a/rustsat/src/lib.rs
+++ b/rustsat/src/lib.rs
@@ -33,6 +33,7 @@
 //! | `rustsat` | The main library, containing basic types, traits, encodings, parsers, and more. |
 //! | `rustsat-tools` | A collection of small helpful tools based on RustSAT that can be installed as binaries. For a list of available tools, see [this directory](https://github.com/chrjabs/rustsat/tree/main/tools/src/bin) with short descriptions of the tools in the headers of the files. |
 //! | `rustsat-<satsolver>` | Interfaces to SAT solvers that can be used alongside `rustsat`. Currently interfaces are available for `cadical`, `kissat`, `glucose`, and `minisat`. |
+//! | `rustsat-ipasir` | [IPASIR](https://github.com/biotomas/ipasir) bindings to use any compliant solver with `rustsat`. |
 //!
 //! ## Installation
 //!
@@ -48,7 +49,6 @@
 //! | --- | --- |
 //! | `internals` | Make some internal data structures for e.g. encodings public. This is useful when basing a more complex encoding on the `rustsat` implementation of another encoding. Note that the internal API might change between releases. |
 //! | `fxhash` | Use the faster firefox hash function from `rustc-hash` in `rustsat`. |
-//! | `ipasir` | Include and link the IPASIR solver interface. |
 //! | `optimization` | Include optimization (MaxSAT) data structures etc. |
 //! | `multiopt` | Include data structures etc. for multi-objective optimization. |
 //! | `compression` | Enable parsing and writing compressed input. |
diff --git a/rustsat/src/solvers.rs b/rustsat/src/solvers.rs
index 82e24ff2..cc979a8a 100644
--- a/rustsat/src/solvers.rs
+++ b/rustsat/src/solvers.rs
@@ -79,27 +79,8 @@
 //! ### IPASIR
 //!
 //! [IPASIR](https://github.com/biotomas/ipasir) is a C API for incremental SAT
-//! solvers. RustSAT's IPASIR interface is disabled by default since linking to
-//! multiple solvers implementing IPASIR at the same time is not possible. The
-//! main reason for including the IPASIR interface in RustSAT is to make it
-//! easier to include solvers that don't have Rust interface crates. For this,
-//! make sure to not depend on any other SAT solver crate to avoid potential
-//! namespace conflicts. Then enable the `ipasir` feature and modify the
-//! following lines in the build script `build.rs` accordingly.
-//!
-//! ```text
-//! // Link to custom IPASIR solver
-//! // Modify this for linking to your static library
-//! // Uncomment and modify this for linking to your static library
-//! // The name of the library should be _without_ the prefix 'lib' and the suffix '.a'
-//! //println!("cargo:rustc-link-lib=static=<path-to-your-static-lib>");
-//! //println!("cargo:rustc-link-search=<name-of-your-static-lib>");
-//! // If your IPASIR solver links to the C++ stdlib, uncomment the next four lines
-//! //#[cfg(target_os = "macos")]
-//! //println!("cargo:rustc-flags=-l dylib=c++");
-//! //#[cfg(not(target_os = "macos"))]
-//! //println!("cargo:rustc-flags=-l dylib=stdc++");
-//! ```
+//! solvers. IPASIR bindings for rustsat are provided in the
+//! [`rustsat-ipasir`](https://crates.io/crates/rustsat-ipasir) crate.
 
 use crate::{
     clause,
@@ -110,11 +91,6 @@ use crate::{
 };
 use core::time::Duration;
 use std::fmt;
-
-#[cfg(feature = "ipasir")]
-mod ipasir;
-#[cfg(feature = "ipasir")]
-pub use ipasir::IpasirSolver;
 use thiserror::Error;
 
 /// Trait for all SAT solvers in this library.
@@ -125,7 +101,7 @@ pub trait Solve: Extend<Clause> {
     fn signature(&self) -> &'static str;
     /// Reserves memory in the solver until a maximum variables, if the solver
     /// supports it
-    fn reserve(&mut self, _max_var: Var) -> SolveMightFail {
+    fn reserve(&mut self, _max_var: Var) -> anyhow::Result<()> {
         Ok(())
     }
     /// Solves the internal CNF formula without any assumptions.
@@ -140,14 +116,14 @@ pub trait Solve: Extend<Clause> {
     /// let res = solver.solve().unwrap();
     /// debug_assert_eq!(res, SolverResult::Sat);
     /// ```
-    fn solve(&mut self) -> Result<SolverResult, SolverError>;
+    fn solve(&mut self) -> anyhow::Result<SolverResult>;
     /// Gets a solution found by the solver up to a specified highest variable.
     ///
     /// # Errors
     ///
     /// - If the solver is not in the satisfied state
     /// - A specific implementation might return other errors
-    fn solution(&self, high_var: Var) -> Result<Assignment, SolverError> {
+    fn solution(&self, high_var: Var) -> anyhow::Result<Assignment> {
         let mut assignment = Vec::new();
         let len = high_var.idx32() + 1;
         assignment.reserve(len as usize);
@@ -164,7 +140,7 @@ pub trait Solve: Extend<Clause> {
     ///
     /// - If the solver is not in the satisfied state
     /// - A specific implementation might return other errors
-    fn full_solution(&self) -> Result<Assignment, SolverError>
+    fn full_solution(&self) -> anyhow::Result<Assignment>
     where
         Self: SolveStats,
     {
@@ -178,7 +154,7 @@ pub trait Solve: Extend<Clause> {
         }
     }
     /// Same as [`Solve::lit_val`], but for variables.
-    fn var_val(&self, var: Var) -> Result<TernaryVal, SolverError> {
+    fn var_val(&self, var: Var) -> anyhow::Result<TernaryVal> {
         self.lit_val(var.pos_lit())
     }
     /// Gets an assignment of a variable in the solver.
@@ -198,25 +174,25 @@ pub trait Solve: Extend<Clause> {
     ///
     /// - If the solver is not in the satisfied state
     /// - A specific implementation might return other errors
-    fn lit_val(&self, lit: Lit) -> Result<TernaryVal, SolverError>;
+    fn lit_val(&self, lit: Lit) -> anyhow::Result<TernaryVal>;
     /// Adds a clause to the solver
     /// If the solver is in the satisfied or unsatisfied state before, it is in
     /// the input state afterwards.
-    fn add_clause(&mut self, clause: Clause) -> SolveMightFail;
+    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()>;
     /// Like [`Solve::add_clause`] but for unit clauses (clauses with one literal).
-    fn add_unit(&mut self, lit: Lit) -> SolveMightFail {
+    fn add_unit(&mut self, lit: Lit) -> anyhow::Result<()> {
         self.add_clause(clause![lit])
     }
     /// Like [`Solve::add_clause`] but for clauses with two literals.
-    fn add_binary(&mut self, lit1: Lit, lit2: Lit) -> SolveMightFail {
+    fn add_binary(&mut self, lit1: Lit, lit2: Lit) -> anyhow::Result<()> {
         self.add_clause(clause![lit1, lit2])
     }
     /// Like [`Solve::add_clause`] but for clauses with three literals.
-    fn add_ternary(&mut self, lit1: Lit, lit2: Lit, lit3: Lit) -> SolveMightFail {
+    fn add_ternary(&mut self, lit1: Lit, lit2: Lit, lit3: Lit) -> anyhow::Result<()> {
         self.add_clause(clause![lit1, lit2, lit3])
     }
     /// Adds all clauses from a [`Cnf`] instance.
-    fn add_cnf(&mut self, cnf: Cnf) -> SolveMightFail {
+    fn add_cnf(&mut self, cnf: Cnf) -> anyhow::Result<()> {
         cnf.into_iter().try_for_each(|cl| self.add_clause(cl))
     }
 }
@@ -226,11 +202,11 @@ pub trait Solve: Extend<Clause> {
 /// use them with this library.
 pub trait SolveIncremental: Solve {
     /// Solves the internal CNF formula under assumptions.
-    fn solve_assumps(&mut self, assumps: &[Lit]) -> Result<SolverResult, SolverError>;
+    fn solve_assumps(&mut self, assumps: &[Lit]) -> anyhow::Result<SolverResult>;
     /// Gets a core found by an unsatisfiable query.
     /// A core is a clause entailed by the formula that contains only inverted
     /// literals of the assumptions.
-    fn core(&mut self) -> Result<Vec<Lit>, SolverError>;
+    fn core(&mut self) -> anyhow::Result<Vec<Lit>>;
 }
 
 /// Trait for all solvers that can be terminated by a termination callback.
@@ -273,11 +249,11 @@ pub trait InterruptSolver: Sync {
 /// Trait for all solvers that can force a face for a literal
 pub trait PhaseLit {
     /// Forces the default decision phase of a variable to a certain value
-    fn phase_lit(&mut self, lit: Lit) -> Result<(), SolverError>;
+    fn phase_lit(&mut self, lit: Lit) -> anyhow::Result<()>;
     /// Undoes the effect of a call to [`PhaseLit::phase_lit`]
-    fn unphase_var(&mut self, var: Var) -> Result<(), SolverError>;
+    fn unphase_var(&mut self, var: Var) -> anyhow::Result<()>;
     /// Undoes the effect of a call to [`PhaseLit::phase_lit`]
-    fn unphase_lit(&mut self, lit: Lit) -> Result<(), SolverError> {
+    fn unphase_lit(&mut self, lit: Lit) -> anyhow::Result<()> {
         self.unphase_var(lit.var())
     }
 }
@@ -285,37 +261,37 @@ pub trait PhaseLit {
 /// Trait for freezing and melting variables in solvers with pre-/inprocessing.
 pub trait FreezeVar {
     /// Freezes a variable so that it is not removed in pre-/inprocessing
-    fn freeze_var(&mut self, var: Var) -> Result<(), SolverError>;
+    fn freeze_var(&mut self, var: Var) -> anyhow::Result<()>;
     /// Melts a variable after it had been frozen
-    fn melt_var(&mut self, var: Var) -> Result<(), SolverError>;
+    fn melt_var(&mut self, var: Var) -> anyhow::Result<()>;
     /// Checks if a variable is frozen
-    fn is_frozen(&mut self, var: Var) -> Result<bool, SolverError>;
+    fn is_frozen(&mut self, var: Var) -> anyhow::Result<bool>;
 }
 
 /// Trait for all solvers that can flip a literal in the current assignment
 pub trait FlipLit {
     /// Attempts flipping the literal in the given assignment and returns `true` if successful
-    fn flip_lit(&mut self, lit: Lit) -> Result<bool, SolverError>;
+    fn flip_lit(&mut self, lit: Lit) -> anyhow::Result<bool>;
     /// Checks if the literal can be flipped in the given assignment without flipping it
-    fn is_flippable(&mut self, lit: Lit) -> Result<bool, SolverError>;
+    fn is_flippable(&mut self, lit: Lit) -> anyhow::Result<bool>;
 }
 
 /// Trait for all solvers that can limit the number of conflicts
 pub trait LimitConflicts {
     /// Sets or removes a limit on the number of conflicts
-    fn limit_conflicts(&mut self, limit: Option<u32>) -> Result<(), SolverError>;
+    fn limit_conflicts(&mut self, limit: Option<u32>) -> anyhow::Result<()>;
 }
 
 /// Trait for all solvers that can limit the number of decisions
 pub trait LimitDecisions {
     /// Sets or removes a limit on the number of decisions
-    fn limit_decisions(&mut self, limit: Option<u32>) -> Result<(), SolverError>;
+    fn limit_decisions(&mut self, limit: Option<u32>) -> anyhow::Result<()>;
 }
 
 /// Trait for all solvers that can limit the number of propagations
 pub trait LimitPropagations {
     /// Sets or removes a limit on the number of propagations
-    fn limit_propagations(&mut self, limit: Option<u32>) -> Result<(), SolverError>;
+    fn limit_propagations(&mut self, limit: Option<u32>) -> anyhow::Result<()>;
 }
 
 /// Trait for all solvers allowing access to internal search statistics
@@ -328,9 +304,6 @@ pub trait GetInternalStats {
     fn conflicts(&self) -> usize;
 }
 
-/// Return type of solver calls that don't return but might fail
-pub type SolveMightFail = Result<(), SolverError>;
-
 #[allow(dead_code)]
 type TermCallbackPtr<'a> = Box<dyn FnMut() -> ControlSignal + 'a>;
 #[allow(dead_code)]
@@ -410,7 +383,7 @@ pub trait SolveStats {
 }
 
 /// States that the solver can be in.
-#[derive(Debug, Clone, PartialEq, Eq)]
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
 pub enum SolverState {
     /// Configuration of the solver must be done in this state, before any clauses are added
     Configuring,
@@ -420,9 +393,6 @@ pub enum SolverState {
     Sat,
     /// The query was found unsatisfiable.
     Unsat,
-    /// Solver is in error state.
-    /// For example after trying to add a clause to a non-incremental solver after solving.
-    Error(String),
 }
 
 impl fmt::Display for SolverState {
@@ -432,7 +402,6 @@ impl fmt::Display for SolverState {
             SolverState::Input => write!(f, "INPUT"),
             SolverState::Sat => write!(f, "SAT"),
             SolverState::Unsat => write!(f, "UNSAT"),
-            SolverState::Error(desc) => write!(f, "Error: {}", desc),
         }
     }
 }
@@ -467,15 +436,21 @@ pub enum ControlSignal {
     Terminate,
 }
 
-/// Type representing solver errors
+/// A solver state error
 #[derive(Error, Debug, Clone, PartialEq, Eq)]
-pub enum SolverError {
-    /// An API with a description
-    #[error("API error: {0}")]
-    Api(String),
-    /// The solver was expected to be in the second [`SolverState`], but it is in the first.
-    #[error("solvers needs to be in state {1} but was in state {0}")]
-    State(SolverState, SolverState),
+pub struct StateError {
+    pub required_state: SolverState,
+    pub actual_state: SolverState,
+}
+
+impl fmt::Display for StateError {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(
+            f,
+            "action requires {} state, but solver is in state {}",
+            self.required_state, self.actual_state
+        )
+    }
 }
 
 impl<S: Solve + SolveStats> CollectClauses for S {
diff --git a/rustsat/src/types.rs b/rustsat/src/types.rs
index 8e5c356c..46c131af 100644
--- a/rustsat/src/types.rs
+++ b/rustsat/src/types.rs
@@ -139,13 +139,28 @@ impl Var {
         self.idx
     }
 
-    /// Converts the variable to an integer as accepted by the IPASIR API and
-    /// similar. The IPASIR variable will have idx+1. Panics if the literal does not fit into a `c_int`.
+    /// Converts the variable to an integer as accepted by
+    /// [IPASIR](https://github.com/biotomas/ipasir) and the [DIMACS file
+    /// format](http://www.satcompetition.org/2011/format-benchmarks2011.html). The IPASIR variable
+    /// will have idx+1. Panics if the literal does not fit into a `c_int`.
     pub fn to_ipasir(self) -> c_int {
-        (self.idx() + 1)
+        (self.idx32() + 1)
             .try_into()
             .expect("variable index too high to fit in c_int")
     }
+
+    /// Converts the variable to an integer as accepted by
+    /// [IPASIR](https://github.com/biotomas/ipasir) and the [DIMACS file
+    /// format](http://www.satcompetition.org/2011/format-benchmarks2011.html). The IPASIR literal
+    /// will have idx+1 and be negative if the literal is negated. Returns
+    /// `Err(TypeError::IdxTooHigh(_, _))` if the literal does not fit into a `c_int`. As [`c_int`
+    /// will almost always be `i32`](https://doc.rust-lang.org/std/os/raw/type.c_int.html), it is
+    /// mostly safe to simply use [`to_ipasir`] instead.
+    pub fn to_ipasir_with_error(self) -> Result<c_int, TypeError> {
+        (self.idx32() + 1)
+            .try_into()
+            .map_err(|_| TypeError::IdxTooHigh(self.idx32() + 1, c_int::MAX as u32))
+    }
 }
 
 /// Incrementing variables
@@ -205,14 +220,17 @@ macro_rules! var {
 }
 
 /// Type representing literals, possibly negated boolean variables.
+///
+/// # Representation in Memory
+///
+/// Literal representation is `idx << 1` with the last bit representing
+/// whether the literal is negated or not. This way the literal can directly
+/// be used to index data structures with the two literals of a variable
+/// being close together.
 #[cfg_attr(feature = "pyapi", pyclass)]
 #[derive(Hash, Eq, PartialEq, PartialOrd, Ord, Clone, Copy, Debug)]
 #[repr(transparent)]
 pub struct Lit {
-    /// Literal representation is `idx << 1` with the last bit representing
-    /// whether the literal is negated or not. This way the literal can directly
-    /// be used to index data structures with the two literals of a variable
-    /// being close together.
     lidx: u32,
 }
 
@@ -270,14 +288,14 @@ impl Lit {
     }
 
     /// Creates a new positive literal with a given index.
-    /// Panics if `idx > Var::MAX_IDX`.
+    /// Returns an error if `idx > Var::MAX_IDX`.
     #[inline]
     pub fn positive_with_error(idx: u32) -> Result<Lit, TypeError> {
         Lit::new_with_error(idx, false)
     }
 
     /// Creates a new negated literal with a given index.
-    /// Panics if `idx > Var::MAX_IDX`.
+    /// Returns an error if `idx > Var::MAX_IDX`.
     #[inline]
     pub fn negative_with_error(idx: u32) -> Result<Lit, TypeError> {
         Lit::new_with_error(idx, true)
@@ -299,8 +317,9 @@ impl Lit {
         Lit::new_unchecked(idx, true)
     }
 
-    /// Create a literal from an IPASIR integer value. Returns an error if
-    /// the value is zero or the index too high.
+    /// Create a literal from an
+    /// [IPASIR](https://github.com/biotomas/ipasir)/[DIMACS](http://www.satcompetition.org/2011/format-benchmarks2011.html)
+    /// integer value. Returns an error if the value is zero or the index too high.
     pub fn from_ipasir(val: c_int) -> Result<Lit, TypeError> {
         if val == 0 {
             return Err(TypeError::IpasirZero);
@@ -355,9 +374,11 @@ impl Lit {
         (self.lidx & 1u32) == 1
     }
 
-    /// Converts the literal to an integer as accepted by the IPASIR API and
-    /// similar. The IPASIR literal will have idx+1 and be negative if the
-    /// literal is negated. Panics if the literal does not fit into a `c_int`.
+    /// Converts the literal to an integer as accepted by
+    /// [IPASIR](https://github.com/biotomas/ipasir) and the
+    /// [DIMACS file format](http://www.satcompetition.org/2011/format-benchmarks2011.html). The
+    /// IPASIR literal will have idx+1 and be negative if the literal is negated. Panics if the
+    /// literal does not fit into a `c_int`.
     pub fn to_ipasir(self) -> c_int {
         let negated = self.is_neg();
         let idx: c_int = (self.vidx() + 1)
@@ -370,10 +391,13 @@ impl Lit {
         }
     }
 
-    /// Converts the literal to an integer as accepted by the IPASIR API and
-    /// similar. The IPASIR literal will have idx+1 and be negative if the
-    /// literal is negated. Returns `Err(TypeError::IdxTooHigh(_, _))` if the
-    /// literal does not fit into a `c_int`.
+    /// Converts the literal to an integer as accepted by
+    /// [IPASIR](https://github.com/biotomas/ipasir) and the [DIMACS file
+    /// format](http://www.satcompetition.org/2011/format-benchmarks2011.html). The IPASIR literal
+    /// will have idx+1 and be negative if the literal is negated. Returns
+    /// `Err(TypeError::IdxTooHigh(_, _))` if the literal does not fit into a `c_int`. As [`c_int`
+    /// will almost always be `i32`](https://doc.rust-lang.org/std/os/raw/type.c_int.html), it is
+    /// mostly safe to simply use [`to_ipasir`] instead.
     pub fn to_ipasir_with_error(self) -> Result<c_int, TypeError> {
         let negated = self.is_neg();
         let idx: c_int = match (self.vidx() + 1).try_into() {
@@ -471,7 +495,7 @@ impl Lit {
         hasher.finish()
     }
 
-    /// Gets the IPASIR representation of the literal
+    /// Gets the IPASIR/DIMACS representation of the literal
     #[pyo3(name = "to_ipasir")]
     fn py_ipasir(&self) -> c_int {
         let negated = self.is_neg();
@@ -502,8 +526,9 @@ macro_rules! lit {
     };
 }
 
-/// More easily creates literals with IPASIR indexing (starts from 1) and
-/// negation (negative value is negation). Mainly used in tests.
+/// More easily creates literals with
+/// [IPASIR](https://github.com/biotomas/ipasir)/[DIMACS](http://www.satcompetition.org/2011/format-benchmarks2011.html)
+/// indexing (starts from 1) and negation (negative value is negation). Mainly used in tests.
 ///
 /// # Examples
 ///
@@ -746,8 +771,8 @@ pub enum TypeError {
     /// Contains the requested and the maximum index.
     #[error("index {0} is too high (maximum {1})")]
     IdxTooHigh(u32, u32),
-    /// IPASIR index is zero
-    #[error("zero is an invalid IPASIR literal")]
+    /// IPASIR/DIMACS index is zero
+    #[error("zero is an invalid IPASIR/DIMACS literal")]
     IpasirZero,
 }
 
diff --git a/tools/Cargo.toml b/tools/Cargo.toml
index fde8771b..22c9cc1a 100644
--- a/tools/Cargo.toml
+++ b/tools/Cargo.toml
@@ -12,7 +12,12 @@ readme = "README.md"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-rustsat = { version = "0.4.3", path = "../rustsat", features = ["compression", "multiopt", "rand", "internals"] }
+rustsat = { version = "0.4.3", path = "../rustsat", features = [
+  "compression",
+  "multiopt",
+  "rand",
+  "internals",
+] }
 rustsat-cadical = { version = "0.2.4", path = "../cadical", optional = true }
 rustsat-minisat = { version = "0.2.4", path = "../minisat", optional = true }
 clap = { version = "4.2.4", features = ["derive", "cargo"] }


Test patch:
diff --git a/cadical/test-all.sh b/cadical/test-all.sh
index 015d64d4..afdfed3c 100755
--- a/cadical/test-all.sh
+++ b/cadical/test-all.sh
@@ -84,6 +84,10 @@ echo "Testing v1.9.4"
 cargo test --features=v1-9-4 &> v194-test.log
 echo "v1.9.4 test returned: $?"
 
+echo "Testing v1.9.5"
+cargo test --features=v1-9-5 &> v195-test.log
+echo "v1.9.5 test returned: $?"
+
 echo "Testing quiet"
 cargo test --features=quiet &> quiet-test.log
 echo "quiet test returned: $?"