diff --git a/solver/src/solver/solver_impl.rs b/solver/src/solver/solver_impl.rs index 75c9b7bc..bba2ae2c 100644 --- a/solver/src/solver/solver_impl.rs +++ b/solver/src/solver/solver_impl.rs @@ -597,15 +597,14 @@ impl Solver { pub fn incremental_push_all( &mut self, assumptions: impl IntoIterator, - ) -> Result, (usize, UnsatCore)> { - let mut res_ok = Vec::new(); + ) -> Result<(), (usize, UnsatCore)> { for (i, lit) in assumptions.into_iter().enumerate() { match self.assume_and_propagate(lit) { - Ok(b) => res_ok.push(b), + Ok(_) => (), Err(unsat_core) => return Err((i, unsat_core)), } } - Ok(res_ok) + Ok(()) } /// Incremental solving: Removes the last assumption that was pushed and