diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs
index f20dd3a4e..43d948852 100644
--- a/src/assign/propagate.rs
+++ b/src/assign/propagate.rs
@@ -351,22 +351,23 @@ impl PropagateIF for AssignStack {
             // while the key of watch_cache is watching literals.
             // Therefore keys to access appropriate targets have the opposite phases.
             //
-            for (blocker, cid) in cdb.binary_links(false_lit).iter().copied() {
+            for (blocker, cr) in cdb.binary_links(false_lit).iter() {
+                let b = cr.get();
                 let var = &self.var[blocker.vi()];
-                debug_assert!(!cdb[cid].is_dead());
+                debug_assert!(!b.is_dead());
                 debug_assert!(!var.is(FlagVar::ELIMINATED));
-                debug_assert_ne!(blocker, false_lit);
-                debug_assert_eq!(cdb[cid].len(), 2);
-                match lit_assign!(var, blocker) {
+                debug_assert_ne!(*blocker, false_lit);
+                debug_assert_eq!(b.len(), 2);
+                match lit_assign!(var, *blocker) {
                     Some(true) => (),
                     Some(false) => {
                         check_in!(cid, Propagate::EmitConflict(self.num_conflict + 1, blocker));
-                        conflict_path!(blocker, minimized_reason!(propagating));
+                        conflict_path!(*blocker, minimized_reason!(propagating));
                     }
                     None => {
-                        debug_assert!(cdb[cid].lit0() == false_lit || cdb[cid].lit1() == false_lit);
+                        debug_assert!(b.lit0() == false_lit || b.lit1() == false_lit);
                         self.assign_by_implication(
-                            blocker,
+                            *blocker,
                             minimized_reason!(propagating),
                             #[cfg(feature = "chrono_BT")]
                             self.level[propagating.vi()],
@@ -378,42 +379,42 @@ impl PropagateIF for AssignStack {
             //## normal clause loop
             //
             let mut source = cdb.watch_cache_iter(propagating);
-            'next_clause: while let Some((cid, mut cached)) = source
+            'next_clause: while let Some((cr, mut cached)) = source
                 .next()
                 .map(|index| cdb.fetch_watch_cache_entry(propagating, index))
             {
                 #[cfg(feature = "boundary_check")]
                 debug_assert!(
-                    !cdb[cid].is_dead(),
+                    !cdb[cr].is_dead(),
                     "dead clause in propagation: {:?}",
-                    cdb.is_garbage_collected(cid),
+                    cdb.is_garbage_collected(cr),
                 );
                 debug_assert!(!self.var[cached.vi()].is(FlagVar::ELIMINATED));
                 #[cfg(feature = "maintain_watch_cache")]
                 debug_assert!(
-                    cached == cdb[cid].lit0() || cached == cdb[cid].lit1(),
+                    cached == cdb[cr].lit0() || cached == cdb[cr].lit1(),
                     "mismatch watch literal and its cache {}: l0 {}  l1 {}, timestamp: {:?}",
                     cached,
-                    cdb[cid].lit0(),
-                    cdb[cid].lit1(),
-                    cdb[cid].timestamp(),
+                    cdb[cr].lit0(),
+                    cdb[cr].lit1(),
+                    cdb[cr].timestamp(),
                 );
                 // assert_ne!(other_watch.vi(), false_lit.vi());
-                // assert!(other_watch == cdb[cid].lit0() || other_watch == cdb[cid].lit1());
+                // assert!(other_watch == cdb[cr].lit0() || other_watch == cdb[cr].lit1());
                 let mut other_watch_value = lit_assign!(self.var[cached.vi()], cached);
                 let mut updated_cache: Option<Lit> = None;
                 if Some(true) == other_watch_value {
                     #[cfg(feature = "maintain_watch_cache")]
-                    debug_assert!(cdb[cid].lit0() == cached || cdb[cid].lit1() == cached);
+                    debug_assert!(cdb[cr].lit0() == cached || cdb[cr].lit1() == cached);
 
                     // In this path, we use only `AssignStack::assign`.
                     // assert!(w.blocker == cdb[w.c].lits[0] || w.blocker == cdb[w.c].lits[1]);
                     cdb.transform_by_restoring_watch_cache(propagating, &mut source, None);
-                    check_in!(cid, Propagate::CacheSatisfied(self.num_conflict));
+                    check_in!(cr, Propagate::CacheSatisfied(self.num_conflict));
                     continue 'next_clause;
                 }
                 {
-                    let c = &cdb[cid];
+                    let c = cr.get();
                     let lit0 = c.lit0();
                     let lit1 = c.lit1();
                     let (false_watch_pos, other) = if false_lit == lit1 {
@@ -433,12 +434,11 @@ impl PropagateIF for AssignStack {
                                 &mut source,
                                 Some(other),
                             );
-                            check_in!(cid, Propagate::CacheSatisfied(self.num_conflict));
+                            check_in!(cr, Propagate::CacheSatisfied(self.num_conflict));
                             continue 'next_clause;
                         }
                         updated_cache = Some(other);
                     }
-                    let c = &cdb[cid];
                     debug_assert!(lit0 == false_lit || lit1 == false_lit);
                     //
                     //## Search an un-falsified literal
@@ -454,44 +454,45 @@ impl PropagateIF for AssignStack {
                         if lit_assign!(self.var[lk.vi()], *lk) != Some(false) {
                             let new_watch = !*lk;
                             cdb.detach_watch_cache(propagating, &mut source);
-                            cdb.transform_by_updating_watch(cid, false_watch_pos, k, true);
-                            cdb[cid].search_from = (k + 1) as u16;
+                            cdb.transform_by_updating_watch(cr, false_watch_pos, k, true);
+                            c.search_from = (k + 1) as u16;
                             debug_assert_ne!(self.assigned(new_watch), Some(true));
                             check_in!(
-                                cid,
+                                cr,
                                 Propagate::FindNewWatch(self.num_conflict, propagating, new_watch)
                             );
                             continue 'next_clause;
                         }
                     }
                     if false_watch_pos == 0 {
-                        cdb.swap_watch(cid);
+                        cdb.swap_watch(cr);
                     }
                 }
+                let c = cr.get();
                 cdb.transform_by_restoring_watch_cache(propagating, &mut source, updated_cache);
                 if other_watch_value == Some(false) {
-                    check_in!(cid, Propagate::EmitConflict(self.num_conflict + 1, cached));
-                    conflict_path!(cached, AssignReason::Implication(cid));
+                    check_in!(cr, Propagate::EmitConflict(self.num_conflict + 1, cached));
+                    conflict_path!(cached, AssignReason::Implication(cr));
                 }
 
                 #[cfg(feature = "chrono_BT")]
-                let dl = cdb[cid]
+                let dl = c
                     .iter()
                     .skip(1)
                     .map(|l| self.level[l.vi()])
                     .max()
                     .unwrap_or(self.root_level);
 
-                debug_assert_eq!(cdb[cid].lit0(), cached);
+                debug_assert_eq!(c.lit0(), cached);
                 debug_assert_eq!(self.assigned(cached), None);
                 debug_assert!(other_watch_value.is_none());
                 self.assign_by_implication(
                     cached,
-                    AssignReason::Implication(cid),
+                    AssignReason::Implication(cr),
                     #[cfg(feature = "chrono_BT")]
                     dl,
                 );
-                check_in!(cid, Propagate::BecameUnit(self.num_conflict, cached));
+                check_in!(cr, Propagate::BecameUnit(self.num_conflict, cached));
             }
             from_saved_trail!();
         }
@@ -548,22 +549,23 @@ impl PropagateIF for AssignStack {
             //
             //## binary loop
             //
-            for (blocker, cid) in cdb.binary_links(false_lit).iter().copied() {
-                debug_assert!(!cdb[cid].is_dead());
+            for (blocker, cr) in cdb.binary_links(false_lit).iter() {
+                let c = cr.get();
+                debug_assert!(!c.is_dead());
                 debug_assert!(!self.var[blocker.vi()].is(FlagVar::ELIMINATED));
-                debug_assert_ne!(blocker, false_lit);
+                debug_assert_ne!(*blocker, false_lit);
 
                 #[cfg(feature = "boundary_check")]
-                debug_assert_eq!(cdb[*cid].len(), 2);
+                debug_assert_eq!(c.len(), 2);
 
-                match lit_assign!(self.var[blocker.vi()], blocker) {
+                match lit_assign!(self.var[blocker.vi()], *blocker) {
                     Some(true) => (),
-                    Some(false) => conflict_path!(blocker, AssignReason::BinaryLink(propagating)),
+                    Some(false) => conflict_path!(*blocker, AssignReason::BinaryLink(propagating)),
                     None => {
-                        debug_assert!(cdb[cid].lit0() == false_lit || cdb[cid].lit1() == false_lit);
+                        debug_assert!(c.lit0() == false_lit || c.lit1() == false_lit);
 
                         self.assign_by_implication(
-                            blocker,
+                            *blocker,
                             AssignReason::BinaryLink(propagating),
                             #[cfg(feature = "chrono_BT")]
                             self.level[false_lit.vi()],
@@ -575,11 +577,12 @@ impl PropagateIF for AssignStack {
             //## normal clause loop
             //
             let mut source = cdb.watch_cache_iter(propagating);
-            'next_clause: while let Some((cid, mut cached)) = source
+            'next_clause: while let Some((cr, mut cached)) = source
                 .next()
                 .map(|index| cdb.fetch_watch_cache_entry(propagating, index))
             {
-                if cdb[cid].is_dead() {
+                let c = cr.get();
+                if c.is_dead() {
                     cdb.transform_by_restoring_watch_cache(propagating, &mut source, None);
                     continue;
                 }
@@ -588,11 +591,10 @@ impl PropagateIF for AssignStack {
                 let mut updated_cache: Option<Lit> = None;
                 if matches!(other_watch_value, Some(true)) {
                     cdb.transform_by_restoring_watch_cache(propagating, &mut source, None);
-                    check_in!(cid, Propagate::SandboxCacheSatisfied(self.num_conflict));
+                    check_in!(cr, Propagate::SandboxCacheSatisfied(self.num_conflict));
                     continue 'next_clause;
                 }
                 {
-                    let c = &cdb[cid];
                     let lit0 = c.lit0();
                     let lit1 = c.lit1();
                     let (false_watch_pos, other) = if false_lit == lit1 {
@@ -611,12 +613,11 @@ impl PropagateIF for AssignStack {
                                 &mut source,
                                 Some(other),
                             );
-                            check_in!(cid, Propagate::SandboxCacheSatisfied(self.num_conflict));
+                            check_in!(cr, Propagate::SandboxCacheSatisfied(self.num_conflict));
                             continue 'next_clause;
                         }
                         updated_cache = Some(other);
                     }
-                    let c = &cdb[cid];
                     debug_assert!(lit0 == false_lit || lit1 == false_lit);
                     let start = c.search_from;
                     for (k, lk) in c
@@ -628,14 +629,14 @@ impl PropagateIF for AssignStack {
                         if lit_assign!(self.var[lk.vi()], *lk) != Some(false) {
                             let new_watch = !*lk;
                             cdb.detach_watch_cache(propagating, &mut source);
-                            cdb.transform_by_updating_watch(cid, false_watch_pos, k, true);
-                            cdb[cid].search_from = (k as u16).saturating_add(1);
+                            cdb.transform_by_updating_watch(cr, false_watch_pos, k, true);
+                            c.search_from = (k as u16).saturating_add(1);
                             debug_assert!(
                                 self.assigned(!new_watch) == Some(true)
                                     || self.assigned(!new_watch).is_none()
                             );
                             check_in!(
-                                cid,
+                                cr,
                                 Propagate::SandboxFindNewWatch(
                                     self.num_conflict,
                                     false_lit,
@@ -646,36 +647,36 @@ impl PropagateIF for AssignStack {
                         }
                     }
                     if false_watch_pos == 0 {
-                        cdb.swap_watch(cid);
+                        cdb.swap_watch(cr);
                     }
                 }
                 cdb.transform_by_restoring_watch_cache(propagating, &mut source, updated_cache);
                 if other_watch_value == Some(false) {
                     check_in!(
-                        cid,
+                        cr,
                         Propagate::SandboxEmitConflict(self.num_conflict, propagating)
                     );
-                    return Err((cached, AssignReason::Implication(cid)));
+                    return Err((cached, AssignReason::Implication(cr)));
                 }
 
                 #[cfg(feature = "chrono_BT")]
-                let dl = cdb[cid]
+                let dl = cdb[cr]
                     .iter()
                     .skip(1)
                     .map(|l| self.level[l.vi()])
                     .max()
                     .unwrap_or(self.root_level);
-                debug_assert_eq!(cdb[cid].lit0(), cached);
+                debug_assert_eq!(c.lit0(), cached);
                 debug_assert_eq!(self.assigned(cached), None);
                 debug_assert!(other_watch_value.is_none());
 
                 self.assign_by_implication(
                     cached,
-                    AssignReason::Implication(cid),
+                    AssignReason::Implication(cr),
                     #[cfg(feature = "chrono_BT")]
                     dl,
                 );
-                check_in!(cid, Propagate::SandboxBecameUnit(self.num_conflict));
+                check_in!(cr, Propagate::SandboxBecameUnit(self.num_conflict));
             }
         }
         Ok(())
@@ -714,15 +715,13 @@ impl AssignStack {
         let mut num_propagated = 0;
         while num_propagated < self.trail.len() {
             num_propagated = self.trail.len();
-            for ci in 1..cdb.len() {
-                let cid = ClauseRef::from(ci);
-                if cdb[cid].is_dead() {
+            for cr in cdb.iter() {
+                let c = cr.get();
+                if c.is_dead() {
                     continue;
                 }
-                debug_assert!(cdb[cid]
-                    .iter()
-                    .all(|l| !self.var[l.vi()].is(FlagVar::ELIMINATED)));
-                match cdb.transform_by_simplification(self, cid) {
+                debug_assert!(c.iter().all(|l| !self.var[l.vi()].is(FlagVar::ELIMINATED)));
+                match cdb.transform_by_simplification(self, *cr) {
                     RefClause::Clause(_) => (),
                     RefClause::Dead => (), // was a satisfied clause
                     RefClause::EmptyClause => return Err(SolverError::EmptyClause),
@@ -731,7 +730,7 @@ impl AssignStack {
                         debug_assert!(self.assigned(lit).is_none());
                         cdb.certificate_add_assertion(lit);
                         self.assign_at_root_level(lit)?;
-                        cdb.remove_clause(cid);
+                        cdb.remove_clause(*cr);
                     }
                 }
             }
diff --git a/src/assign/trail_saving.rs b/src/assign/trail_saving.rs
index 037091372..26d76164e 100644
--- a/src/assign/trail_saving.rs
+++ b/src/assign/trail_saving.rs
@@ -79,13 +79,14 @@ impl TrailSavingIF for AssignStack {
                     );
                 }
                 // reason refinement by ignoring this dependecy
-                (None, AssignReason::Implication(c)) if q < cdb[c].rank => {
+                (None, AssignReason::Implication(cr)) if q < cr.get().rank => {
                     self.insert_heap(vi);
                     return self.truncate_trail_saved(i + 1);
                 }
-                (None, AssignReason::Implication(cid)) => {
-                    debug_assert_eq!(cdb[cid].lit0(), lit);
-                    debug_assert!(cdb[cid]
+                (None, AssignReason::Implication(cr)) => {
+                    debug_assert_eq!(cr.get().lit0(), lit);
+                    debug_assert!(cr
+                        .get()
                         .iter()
                         .skip(1)
                         .all(|l| self.assigned(*l) == Some(false)));
@@ -105,11 +106,12 @@ impl TrailSavingIF for AssignStack {
                     self.clear_saved_trail();
                     return Err((lit, old_reason));
                 }
-                (Some(false), AssignReason::Implication(cid)) => {
-                    debug_assert!(cdb[cid].iter().all(|l| self.assigned(*l) == Some(false)));
+                (Some(false), AssignReason::Implication(cr)) => {
+                    let c = cr.get();
+                    debug_assert!(c.iter().all(|l| self.assigned(*l) == Some(false)));
                     let _ = self.truncate_trail_saved(i + 1); // reduce heap ops.
                     self.clear_saved_trail();
-                    return Err((cdb[cid].lit0(), AssignReason::Implication(cid)));
+                    return Err((c.lit0(), AssignReason::Implication(cr)));
                 }
                 (_, AssignReason::Decision(lvl)) => {
                     debug_assert_ne!(0, lvl);
diff --git a/src/cdb/db.rs b/src/cdb/db.rs
index 7ee0af2d8..3e60ba9b6 100644
--- a/src/cdb/db.rs
+++ b/src/cdb/db.rs
@@ -9,6 +9,7 @@ use {
     },
     crate::{assign::AssignIF, types::*},
     std::{
+        collections::HashSet,
         num::NonZeroU32,
         ops::{Index, IndexMut, Range, RangeFrom},
         slice::Iter,
@@ -21,7 +22,7 @@ use std::{fs::File, io::Write, path::Path};
 impl Default for ClauseDB {
     fn default() -> ClauseDB {
         ClauseDB {
-            clause: Vec::new(),
+            clause: HashSet::new(),
             binary_link: BinaryLinkDB::default(),
             watch_cache: Vec::new(),
             certification_store: CertificationStore::default(),
@@ -82,82 +83,82 @@ impl Default for ClauseDB {
 //     }
 // }
 
-impl Index<&ClauseRef> for ClauseDB {
-    type Output = Clause;
-    #[inline]
-    fn index(&self, cid: &ClauseRef) -> &Clause {
-        let i = NonZeroU32::get(cid.ordinal) as usize;
-        #[cfg(feature = "unsafe_access")]
-        unsafe {
-            self.clause.get_unchecked(i)
-        }
-        #[cfg(not(feature = "unsafe_access"))]
-        &self.clause[i]
-    }
-}
+// impl Index<&ClauseRef> for ClauseDB {
+//     type Output = Clause;
+//     #[inline]
+//     fn index(&self, cid: &ClauseRef) -> &Clause {
+//         let i = NonZeroU32::get(cid.ordinal) as usize;
+//         #[cfg(feature = "unsafe_access")]
+//         unsafe {
+//             self.clause.get_unchecked(i)
+//         }
+//         #[cfg(not(feature = "unsafe_access"))]
+//         &self.clause[i]
+//     }
+// }
 
-impl IndexMut<&ClauseRef> for ClauseDB {
-    #[inline]
-    fn index_mut(&mut self, cid: &ClauseRef) -> &mut Clause {
-        let i = NonZeroU32::get(cid.ordinal) as usize;
-        #[cfg(feature = "unsafe_access")]
-        unsafe {
-            self.clause.get_unchecked_mut(i)
-        }
-        #[cfg(not(feature = "unsafe_access"))]
-        &mut self.clause[i]
-    }
-}
+// impl IndexMut<&ClauseRef> for ClauseDB {
+//     #[inline]
+//     fn index_mut(&mut self, cid: &ClauseRef) -> &mut Clause {
+//         let i = NonZeroU32::get(cid.ordinal) as usize;
+//         #[cfg(feature = "unsafe_access")]
+//         unsafe {
+//             self.clause.get_unchecked_mut(i)
+//         }
+//         #[cfg(not(feature = "unsafe_access"))]
+//         &mut self.clause[i]
+//     }
+// }
 
-impl Index<Range<usize>> for ClauseDB {
-    type Output = [Clause];
-    #[inline]
-    fn index(&self, r: Range<usize>) -> &[Clause] {
-        #[cfg(feature = "unsafe_access")]
-        unsafe {
-            self.clause.get_unchecked(r)
-        }
-        #[cfg(not(feature = "unsafe_access"))]
-        &self.clause[r]
-    }
-}
+// impl Index<Range<usize>> for ClauseDB {
+//     type Output = [Clause];
+//     #[inline]
+//     fn index(&self, r: Range<usize>) -> &[Clause] {
+//         #[cfg(feature = "unsafe_access")]
+//         unsafe {
+//             self.clause.get_unchecked(r)
+//         }
+//         #[cfg(not(feature = "unsafe_access"))]
+//         &self.clause[r]
+//     }
+// }
 
-impl Index<RangeFrom<usize>> for ClauseDB {
-    type Output = [Clause];
-    #[inline]
-    fn index(&self, r: RangeFrom<usize>) -> &[Clause] {
-        #[cfg(feature = "unsafe_access")]
-        unsafe {
-            self.clause.get_unchecked(r)
-        }
-        #[cfg(not(feature = "unsafe_access"))]
-        &self.clause[r]
-    }
-}
+// impl Index<RangeFrom<usize>> for ClauseDB {
+//     type Output = [Clause];
+//     #[inline]
+//     fn index(&self, r: RangeFrom<usize>) -> &[Clause] {
+//         #[cfg(feature = "unsafe_access")]
+//         unsafe {
+//             self.clause.get_unchecked(r)
+//         }
+//         #[cfg(not(feature = "unsafe_access"))]
+//         &self.clause[r]
+//     }
+// }
 
-impl IndexMut<Range<usize>> for ClauseDB {
-    #[inline]
-    fn index_mut(&mut self, r: Range<usize>) -> &mut [Clause] {
-        #[cfg(feature = "unsafe_access")]
-        unsafe {
-            self.clause.get_unchecked_mut(r)
-        }
-        #[cfg(not(feature = "unsafe_access"))]
-        &mut self.clause[r]
-    }
-}
+// impl IndexMut<Range<usize>> for ClauseDB {
+//     #[inline]
+//     fn index_mut(&mut self, r: Range<usize>) -> &mut [Clause] {
+//         #[cfg(feature = "unsafe_access")]
+//         unsafe {
+//             self.clause.get_unchecked_mut(r)
+//         }
+//         #[cfg(not(feature = "unsafe_access"))]
+//         &mut self.clause[r]
+//     }
+// }
 
-impl IndexMut<RangeFrom<usize>> for ClauseDB {
-    #[inline]
-    fn index_mut(&mut self, r: RangeFrom<usize>) -> &mut [Clause] {
-        #[cfg(feature = "unsafe_access")]
-        unsafe {
-            self.clause.get_unchecked_mut(r)
-        }
-        #[cfg(not(feature = "unsafe_access"))]
-        &mut self.clause[r]
-    }
-}
+// impl IndexMut<RangeFrom<usize>> for ClauseDB {
+//     #[inline]
+//     fn index_mut(&mut self, r: RangeFrom<usize>) -> &mut [Clause] {
+//         #[cfg(feature = "unsafe_access")]
+//         unsafe {
+//             self.clause.get_unchecked_mut(r)
+//         }
+//         #[cfg(not(feature = "unsafe_access"))]
+//         &mut self.clause[r]
+//     }
+// }
 
 impl Instantiate for ClauseDB {
     fn instantiate(config: &Config, cnf: &CNFDescription) -> ClauseDB {
diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs
index 58402a42a..7c6cee3dc 100644
--- a/src/cdb/mod.rs
+++ b/src/cdb/mod.rs
@@ -126,13 +126,13 @@ pub trait ClauseDBIF:
     fn new_clause(&mut self, asg: &mut impl AssignIF, v: &mut Vec<Lit>, learnt: bool) -> RefClause;
     fn new_clause_sandbox(&mut self, asg: &mut impl AssignIF, v: &mut Vec<Lit>) -> RefClause;
     /// un-register a clause `cid` from clause database and make the clause dead.
-    fn remove_clause(&mut self, cid: ClauseRef);
+    fn remove_clause(&mut self, cr: ClauseRef);
     /// un-register a clause `cid` from clause database and make the clause dead.
-    fn remove_clause_sandbox(&mut self, cid: ClauseRef);
+    fn remove_clause_sandbox(&mut self, cr: ClauseRef);
     /// update watches of the clause
-    fn transform_by_elimination(&mut self, cid: ClauseRef, p: Lit) -> RefClause;
+    fn transform_by_elimination(&mut self, cr: ClauseRef, p: Lit) -> RefClause;
     /// generic clause transformer (not in use)
-    fn transform_by_replacement(&mut self, cid: ClauseRef, vec: &mut Vec<Lit>) -> RefClause;
+    fn transform_by_replacement(&mut self, cr: ClauseRef, vec: &mut Vec<Lit>) -> RefClause;
     /// check satisfied and nullified literals in a clause
     fn transform_by_simplification(&mut self, asg: &mut impl AssignIF, cid: ClauseRef)
         -> RefClause;
diff --git a/src/processor/subsume.rs b/src/processor/subsume.rs
index 5e5d0fcc2..097c5e847 100644
--- a/src/processor/subsume.rs
+++ b/src/processor/subsume.rs
@@ -16,30 +16,30 @@ impl Eliminator {
         &mut self,
         asg: &mut impl AssignIF,
         cdb: &mut impl ClauseDBIF,
-        cid: ClauseRef,
-        did: ClauseRef,
+        mut cr: ClauseRef,
+        mut dr: ClauseRef,
     ) -> MaybeInconsistent {
-        match have_subsuming_lit(cdb, cid, did) {
+        match have_subsuming_lit(cdb, cr, dr) {
             Subsumable::Success => {
                 #[cfg(feature = "trace_elimination")]
                 println!(
                     "BackSubsC    => {} {} subsumed completely by {} {:#}",
-                    did, cdb[did], cid, cdb[cid],
+                    dr, cdb[dr], cr, cdb[cr],
                 );
-                debug_assert!(!cdb[did].is_dead());
-                if !cdb[did].is(FlagClause::LEARNT) {
-                    cdb[cid].turn_off(FlagClause::LEARNT);
+                debug_assert!(!dr.get().is_dead());
+                if !dr.get().is(FlagClause::LEARNT) {
+                    cr.get().turn_off(FlagClause::LEARNT);
                 }
-                self.remove_cid_occur(asg, did, &mut cdb[did]);
-                cdb.remove_clause(did);
+                self.remove_cid_occur(asg, dr, &mut dr.get_mut());
+                cdb.remove_clause(dr);
                 self.num_subsumed += 1;
             }
             // To avoid making a big clause, we have to add a condition for combining them.
             Subsumable::By(l) => {
-                debug_assert!(cid.is_lifted_lit());
+                debug_assert!(cr.is_lifted_lit());
                 #[cfg(feature = "trace_elimination")]
-                println!("BackSubC subsumes {} from {} and {}", l, cid, did);
-                strengthen_clause(asg, cdb, self, did, !l)?;
+                println!("BackSubC subsumes {} from {} and {}", l, cr, dr);
+                strengthen_clause(asg, cdb, self, dr, !l)?;
                 self.enqueue_var(asg, l.vi(), true);
             }
             Subsumable::None => (),
@@ -49,11 +49,11 @@ impl Eliminator {
 }
 
 /// returns a literal if these clauses can be merged by the literal.
-fn have_subsuming_lit(cdb: &mut impl ClauseDBIF, cid: ClauseRef, other: ClauseRef) -> Subsumable {
+fn have_subsuming_lit(cdb: &mut impl ClauseDBIF, cr: ClauseRef, other: ClauseRef) -> Subsumable {
     debug_assert!(!other.is_lifted_lit());
-    if cid.is_lifted_lit() {
-        let l = Lit::from(cid);
-        let oh = &cdb[other];
+    if cr.is_lifted_lit() {
+        let l = Lit::from(cr);
+        let oh = other.get();
         for lo in oh.iter() {
             if l == !*lo {
                 return Subsumable::By(l);
@@ -62,9 +62,9 @@ fn have_subsuming_lit(cdb: &mut impl ClauseDBIF, cid: ClauseRef, other: ClauseRe
         return Subsumable::None;
     }
     // let mut ret: Subsumable = Subsumable::Success;
-    let ch = &cdb[cid];
+    let ch = cr.get();
     debug_assert!(1 < ch.len());
-    let ob = &cdb[other];
+    let ob = other.get();
     debug_assert!(1 < ob.len());
     debug_assert!(ob.contains(ob[0]));
     debug_assert!(ob.contains(ob[1]));
@@ -89,29 +89,30 @@ fn strengthen_clause(
     asg: &mut impl AssignIF,
     cdb: &mut impl ClauseDBIF,
     elim: &mut Eliminator,
-    cid: ClauseRef,
+    mut cr: ClauseRef,
     l: Lit,
 ) -> MaybeInconsistent {
-    debug_assert!(!cdb[cid].is_dead());
-    debug_assert!(1 < cdb[cid].len());
-    match cdb.transform_by_elimination(cid, l) {
+    let mut c = cr.get_mut();
+    debug_assert!(!c.is_dead());
+    debug_assert!(1 < c.len());
+    match cdb.transform_by_elimination(cr, l) {
         RefClause::Clause(_ci) => {
             #[cfg(feature = "trace_elimination")]
-            println!("cid {} drops literal {}", cid, l);
+            println!("cr {} drops literal {}", cr, l);
 
-            elim.enqueue_clause(cid, &mut cdb[cid]);
-            elim.remove_lit_occur(asg, l, cid);
+            elim.enqueue_clause(cr, &mut c);
+            elim.remove_lit_occur(asg, l, cr);
             Ok(())
         }
         RefClause::RegisteredClause(_) => {
-            elim.remove_cid_occur(asg, cid, &mut cdb[cid]);
-            cdb.remove_clause(cid);
+            elim.remove_cid_occur(asg, cr, &mut c);
+            cdb.remove_clause(cr);
             Ok(())
         }
         RefClause::UnitClause(l0) => {
             cdb.certificate_add_assertion(l0);
-            elim.remove_cid_occur(asg, cid, &mut cdb[cid]);
-            cdb.remove_clause(cid);
+            elim.remove_cid_occur(asg, cr, &mut c);
+            cdb.remove_clause(cr);
             match asg.assigned(l0) {
                 None => asg.assign_at_root_level(l0),
                 Some(true) => Ok(()),
diff --git a/src/solver/conflict.rs b/src/solver/conflict.rs
index 112f56aab..17f0f13d4 100644
--- a/src/solver/conflict.rs
+++ b/src/solver/conflict.rs
@@ -173,12 +173,13 @@ pub fn handle_conflict(
     );
     let rank: u16;
     match cdb.new_clause(asg, new_learnt, true) {
-        RefClause::Clause(cid) if learnt_len == 2 => {
+        RefClause::Clause(cr) if learnt_len == 2 => {
+            let c = cr.get();
             #[cfg(feature = "boundary_check")]
-            cdb[cid].set_birth(asg.num_conflict);
+            cdb[cr].set_birth(asg.num_conflict);
 
-            debug_assert_eq!(l0, cdb[cid].lit0());
-            debug_assert_eq!(l1, cdb[cid].lit1());
+            debug_assert_eq!(l0, c.lit0());
+            debug_assert_eq!(l1, c.lit1());
             debug_assert_eq!(asg.assigned(l1), Some(false));
             debug_assert_eq!(asg.assigned(l0), None);
 
@@ -189,39 +190,38 @@ pub fn handle_conflict(
                 assign_level,
             );
             // || check_graph(asg, cdb, l0, "biclause");
-            for cid in &state.derive20 {
-                cdb[cid].turn_on(FlagClause::DERIVE20);
+            for cr in &state.derive20 {
+                cr.get_mut().turn_on(FlagClause::DERIVE20);
             }
             rank = 1;
             #[cfg(feature = "bi_clause_completion")]
             cdb.complete_bi_clauses(asg);
         }
-        RefClause::Clause(cid) => {
+        RefClause::Clause(cr) => {
+            let c = cr.get();
             #[cfg(feature = "boundary_check")]
-            cdb[cid].set_birth(asg.num_conflict);
+            c.set_birth(asg.num_conflict);
 
-            debug_assert_eq!(cdb[cid].lit0(), l0);
+            debug_assert_eq!(c.lit0(), l0);
             debug_assert_eq!(asg.assigned(l0), None);
             asg.assign_by_implication(
                 l0,
-                AssignReason::Implication(cid),
+                AssignReason::Implication(cr),
                 #[cfg(feature = "chrono_BT")]
                 assign_level,
             );
             // || check_graph(asg, cdb, l0, "clause");
-            rank = cdb[cid].rank;
+            rank = c.rank;
             if rank <= 20 {
-                for cid in &state.derive20 {
-                    cdb[cid].turn_on(FlagClause::DERIVE20);
+                for cr in &state.derive20 {
+                    cdb[cr].turn_on(FlagClause::DERIVE20);
                 }
             }
         }
-        RefClause::RegisteredClause(cid) => {
+        RefClause::RegisteredClause(cr) => {
+            let c = cr.get();
             debug_assert_eq!(learnt_len, 2);
-            debug_assert!(
-                (l0 == cdb[cid].lit0() && l1 == cdb[cid].lit1())
-                    || (l0 == cdb[cid].lit1() && l1 == cdb[cid].lit0())
-            );
+            debug_assert!((l0 == c.lit0() && l1 == c.lit1()) || (l0 == c.lit1() && l1 == c.lit0()));
             debug_assert_eq!(asg.assigned(l1), Some(false));
             debug_assert_eq!(asg.assigned(l0), None);
             rank = 1;
@@ -350,23 +350,24 @@ fn conflict_analyze(
                     conflict_level!(vi);
                 }
             }
-            AssignReason::Implication(cid) => {
+            AssignReason::Implication(cr) => {
                 trace!(
                     "analyze clause {}(first literal: {}) for {}",
-                    cid,
-                    i32::from(cdb[cid].lit0()),
+                    cr,
+                    i32::from(cdb[cr].lit0()),
                     p
                 );
-                debug_assert!(!cdb[cid].is_dead() && 2 < cdb[cid].len());
-                // if !cdb.update_at_analysis(asg, cid) {
-                if !cdb[cid].is(FlagClause::LEARNT) {
-                    state.derive20.push(cid);
+                let c = cr.get();
+                debug_assert!(!c.is_dead() && 2 < c.len());
+                // if !cdb.update_at_analysis(asg, cr) {
+                if !c.is(FlagClause::LEARNT) {
+                    state.derive20.push(cr);
                 }
-                if max_lbd < cdb[cid].rank {
-                    max_lbd = cdb[cid].rank;
-                    cid_with_max_lbd = Some(cid);
+                if max_lbd < c.rank {
+                    max_lbd = c.rank;
+                    cid_with_max_lbd = Some(cr);
                 }
-                for q in cdb[cid].iter().skip(1) {
+                for q in c.iter().skip(1) {
                     let vi = q.vi();
                     validate_vi!(vi);
                     if !asg.var(vi).is(FlagVar::CA_SEEN) {
@@ -533,8 +534,8 @@ impl Lit {
                         }
                     }
                 }
-                AssignReason::Implication(cid) => {
-                    let c = &cdb[cid];
+                AssignReason::Implication(cr) => {
+                    let c = cr.get();
                     for q in &(*c)[1..] {
                         let vi = q.vi();
                         let lv = asg.level(vi);
@@ -635,7 +636,7 @@ fn dumper(asg: &AssignStack, cdb: &ClauseDB, bag: &[Lit]) -> String {
             match asg.reason(l.vi()) {
                 AssignReason::Decision(_) => vec![],
                 AssignReason::BinaryLink(lit) => vec![*l, !lit],
-                AssignReason::Implication(cid) => cdb[cid].iter().copied().collect::<Vec<Lit>>(),
+                AssignReason::Implication(cr) => cr.get().iter().copied().collect::<Vec<Lit>>(),
                 AssignReason::None => vec![],
             },
         )