diff --git a/solver/src/reasoners/sat/clauses/mod.rs b/solver/src/reasoners/sat/clauses/mod.rs
index 95d77e24..c5df694d 100644
--- a/solver/src/reasoners/sat/clauses/mod.rs
+++ b/solver/src/reasoners/sat/clauses/mod.rs
@@ -44,6 +44,11 @@ impl Display for ClauseId {
         write!(f, "{}", usize::from(*self))
     }
 }
+impl std::fmt::Debug for ClauseId {
+    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
+        write!(f, "{}", usize::from(*self))
+    }
+}
 
 #[derive(Clone)]
 pub struct ClauseDb {
diff --git a/solver/src/reasoners/sat/sat_solver.rs b/solver/src/reasoners/sat/sat_solver.rs
index eb51f6bf..0a549dcd 100644
--- a/solver/src/reasoners/sat/sat_solver.rs
+++ b/solver/src/reasoners/sat/sat_solver.rs
@@ -347,6 +347,9 @@ impl SatSolver {
         // process all clauses that have been added since last propagation
         while let Some(PendingClause { clause }) = self.pending_clauses.pop_front() {
             if let Some(conflict) = self.process_arbitrary_clause(clause, model) {
+                // the clause returned is violated before being properly set up.
+                // Add it back to the queue so that it is not forgotten if one is calling the solver again
+                self.pending_clauses.push_front(PendingClause { clause });
                 return Err(conflict);
             }
         }