diff --git a/build.rs b/build.rs
index 54060050..3cb94e62 100644
--- a/build.rs
+++ b/build.rs
@@ -90,7 +90,6 @@ fn build_cadical(repo: &str, branch: &str, commit: &str) -> bool {
             // We specify the build manually here instead of calling make for better portability
             let src_files = glob(&format!("{}/src/*.cpp", cadical_dir_str))
                 .unwrap()
-                .into_iter()
                 .filter_map(|res| {
                     if let Ok(p) = res {
                         if let Some(name) = p.file_name() {
@@ -166,7 +165,6 @@ fn build_kissat(repo: &str, branch: &str, commit: &str) -> bool {
             // We specify the build manually here instead of calling make for better portability
             let src_files = glob(&format!("{}/src/*.c", kissat_dir_str))
                 .unwrap()
-                .into_iter()
                 .filter_map(|res| {
                     if let Ok(p) = res {
                         if let Some(name) = p.file_name() {
diff --git a/src/instances/fio/opb.rs b/src/instances/fio/opb.rs
index ceeb97b5..72a31d1d 100644
--- a/src/instances/fio/opb.rs
+++ b/src/instances/fio/opb.rs
@@ -541,7 +541,7 @@ fn write_card<W: Write>(
                 write!(writer, "-1 x{} ", l.vidx() + opts.first_var_idx)
             }
         })?;
-        writeln!(writer, "{} {};", op, bound as isize - offset)
+        writeln!(writer, "{} {};", op, bound - offset)
     } else {
         let (lits, bound, op) = match card {
             CardConstraint::UB(constr) => {
diff --git a/src/instances/sat.rs b/src/instances/sat.rs
index fa29d08b..cd25b6ca 100644
--- a/src/instances/sat.rs
+++ b/src/instances/sat.rs
@@ -570,7 +570,7 @@ impl<VM: ManageVars> SatInstance<VM> {
                     cards.push(pb.as_card_constr().unwrap());
                     return None;
                 }
-                return Some(pb);
+                Some(pb)
             })
             .collect();
         let cards = cards
@@ -597,7 +597,7 @@ impl<VM: ManageVars> SatInstance<VM> {
                     cnf.add_clause(card.as_clause().unwrap());
                     return None;
                 }
-                return Some(card);
+                Some(card)
             })
             .collect();
         if unsat {
diff --git a/src/solvers/cadical.rs b/src/solvers/cadical.rs
index 0dfee25d..8dccbd6f 100644
--- a/src/solvers/cadical.rs
+++ b/src/solvers/cadical.rs
@@ -529,14 +529,14 @@ impl<'term> Terminate<'term> for CaDiCaL<'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::ccadical_set_terminate(self.handle, cb_ptr, ffi::ccadical_terminate_cb) }
+        unsafe {
+            ffi::ccadical_set_terminate(self.handle, cb_ptr, Some(ffi::ccadical_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::ccadical_set_terminate(self.handle, std::ptr::null(), null_cb) }
+        unsafe { ffi::ccadical_set_terminate(self.handle, std::ptr::null(), None) }
     }
 }
 
@@ -576,16 +576,14 @@ impl<'learn> Learn<'learn> for CaDiCaL<'_, 'learn> {
                 self.handle,
                 cb_ptr,
                 max_len.try_into().unwrap(),
-                ffi::ccadical_learn_cb,
+                Some(ffi::ccadical_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::ccadical_set_learn(self.handle, std::ptr::null(), 0, null_cb) }
+        unsafe { ffi::ccadical_set_learn(self.handle, std::ptr::null(), 0, None) }
     }
 }
 
@@ -948,13 +946,13 @@ mod ffi {
         pub fn ccadical_set_terminate(
             solver: *mut CaDiCaLHandle,
             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 ccadical_set_learn(
             solver: *mut CaDiCaLHandle,
             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)>,
         );
         pub fn ccadical_constrain(solver: *mut CaDiCaLHandle, lit: c_int);
         pub fn ccadical_constraint_failed(solver: *mut CaDiCaLHandle) -> c_int;
diff --git a/src/solvers/glucose4/core.rs b/src/solvers/glucose4/core.rs
index 968799e4..33eeae35 100644
--- a/src/solvers/glucose4/core.rs
+++ b/src/solvers/glucose4/core.rs
@@ -253,23 +253,23 @@ impl PhaseLit for GlucoseCore4 {
 
 impl LimitConflicts for GlucoseCore4 {
     fn limit_conflicts(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
-        Ok(self.set_limit(Limit::Conflicts(if let Some(limit) = limit {
+        self.set_limit(Limit::Conflicts(if let Some(limit) = limit {
             limit as i64
         } else {
             -1
-        })))
+        }));
+        Ok(())
     }
 }
 
 impl LimitPropagations for GlucoseCore4 {
     fn limit_propagations(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
-        Ok(
-            self.set_limit(Limit::Propagations(if let Some(limit) = limit {
-                limit as i64
-            } else {
-                -1
-            })),
-        )
+        self.set_limit(Limit::Propagations(if let Some(limit) = limit {
+            limit as i64
+        } else {
+            -1
+        }));
+        Ok(())
     }
 }
 
diff --git a/src/solvers/glucose4/simp.rs b/src/solvers/glucose4/simp.rs
index 9b15d821..f313c497 100644
--- a/src/solvers/glucose4/simp.rs
+++ b/src/solvers/glucose4/simp.rs
@@ -270,23 +270,23 @@ impl PhaseLit for GlucoseSimp4 {
 
 impl LimitConflicts for GlucoseSimp4 {
     fn limit_conflicts(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
-        Ok(self.set_limit(Limit::Conflicts(if let Some(limit) = limit {
+        self.set_limit(Limit::Conflicts(if let Some(limit) = limit {
             limit as i64
         } else {
             -1
-        })))
+        }));
+        Ok(())
     }
 }
 
 impl LimitPropagations for GlucoseSimp4 {
     fn limit_propagations(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
-        Ok(
-            self.set_limit(Limit::Propagations(if let Some(limit) = limit {
-                limit as i64
-            } else {
-                -1
-            })),
-        )
+        self.set_limit(Limit::Propagations(if let Some(limit) = limit {
+            limit as i64
+        } else {
+            -1
+        }));
+        Ok(())
     }
 }
 
diff --git a/src/solvers/kissat.rs b/src/solvers/kissat.rs
index ee8cf5e5..bc7c1ddc 100644
--- a/src/solvers/kissat.rs
+++ b/src/solvers/kissat.rs
@@ -292,14 +292,12 @@ impl<'term> Terminate<'term> for Kissat<'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::kissat_set_terminate(self.handle, cb_ptr, ffi::kissat_terminate_cb) }
+        unsafe { ffi::kissat_set_terminate(self.handle, cb_ptr, Some(ffi::kissat_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::kissat_set_terminate(self.handle, std::ptr::null(), null_cb) }
+        unsafe { ffi::kissat_set_terminate(self.handle, std::ptr::null(), None) }
     }
 }
 
@@ -484,7 +482,7 @@ mod ffi {
         pub fn kissat_set_terminate(
             solver: *mut KissatHandle,
             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 kissat_terminate(solver: *mut KissatHandle);
         pub fn kissat_reserve(solver: *mut KissatHandle, max_var: c_int);
diff --git a/src/solvers/minisat/core.rs b/src/solvers/minisat/core.rs
index d064fff6..93866e73 100644
--- a/src/solvers/minisat/core.rs
+++ b/src/solvers/minisat/core.rs
@@ -252,23 +252,23 @@ impl PhaseLit for MinisatCore {
 
 impl LimitConflicts for MinisatCore {
     fn limit_conflicts(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
-        Ok(self.set_limit(Limit::Conflicts(if let Some(limit) = limit {
+        self.set_limit(Limit::Conflicts(if let Some(limit) = limit {
             limit as i64
         } else {
             -1
-        })))
+        }));
+        Ok(())
     }
 }
 
 impl LimitPropagations for MinisatCore {
     fn limit_propagations(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
-        Ok(
-            self.set_limit(Limit::Propagations(if let Some(limit) = limit {
-                limit as i64
-            } else {
-                -1
-            })),
-        )
+        self.set_limit(Limit::Propagations(if let Some(limit) = limit {
+            limit as i64
+        } else {
+            -1
+        }));
+        Ok(())
     }
 }
 
diff --git a/src/solvers/minisat/simp.rs b/src/solvers/minisat/simp.rs
index bd4f62d2..e9f3970f 100644
--- a/src/solvers/minisat/simp.rs
+++ b/src/solvers/minisat/simp.rs
@@ -269,23 +269,23 @@ impl PhaseLit for MinisatSimp {
 
 impl LimitConflicts for MinisatSimp {
     fn limit_conflicts(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
-        Ok(self.set_limit(Limit::Conflicts(if let Some(limit) = limit {
+        self.set_limit(Limit::Conflicts(if let Some(limit) = limit {
             limit as i64
         } else {
             -1
-        })))
+        }));
+        Ok(())
     }
 }
 
 impl LimitPropagations for MinisatSimp {
     fn limit_propagations(&mut self, limit: Option<u32>) -> Result<(), SolverError> {
-        Ok(
-            self.set_limit(Limit::Propagations(if let Some(limit) = limit {
-                limit as i64
-            } else {
-                -1
-            })),
-        )
+        self.set_limit(Limit::Propagations(if let Some(limit) = limit {
+            limit as i64
+        } else {
+            -1
+        }));
+        Ok(())
     }
 }
 
diff --git a/src/types/constraints.rs b/src/types/constraints.rs
index 868ce648..8db5749f 100644
--- a/src/types/constraints.rs
+++ b/src/types/constraints.rs
@@ -156,7 +156,7 @@ impl Clause {
                 idx += 1;
             }
         }
-        return Some(self);
+        Some(self)
     }
 }