diff --git a/Cargo.lock b/Cargo.lock index ec623dd7f..57ec2655c 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -528,9 +528,9 @@ dependencies = [ [[package]] name = "unicode-width" -version = "0.1.13" +version = "0.1.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0336d538f7abc86d282a4189614dfaa90810dfc2c6f6427eaf88e16311dd225d" +checksum = "7dd6e30e90baa6f72411720665d41d89b9a3d039dc45b8faea1ddd07f617f6af" [[package]] name = "version_check" diff --git a/src/cdb/clause.rs b/src/cdb/clause.rs index b55326816..cbeb0a768 100644 --- a/src/cdb/clause.rs +++ b/src/cdb/clause.rs @@ -100,8 +100,8 @@ impl Default for Clause { ], lits: vec![Lit::default(), Lit::default()], flags: FlagClause::empty(), - rank: 0, - rank_old: 0, + rank: u32::MAX, + rank_old: u32::MAX, search_from: 2, #[cfg(any(feature = "boundary_check", feature = "clause_rewarding"))] @@ -327,7 +327,10 @@ impl Clause { cnt += 1; } } - self.rank = cnt; - cnt + if cnt < self.rank { + self.rank_old = self.rank; + self.rank = cnt; + } + self.rank } } diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs index 2d15505aa..139ca518c 100644 --- a/src/cdb/mod.rs +++ b/src/cdb/mod.rs @@ -270,7 +270,6 @@ impl ClauseDBIF for ClauseDB { debug_assert_eq!(l1, self[ci].lits[1]); } self.clause[ci].search_from = 0; - self.clause[ci].rank_old = self[ci].rank; self.lbd.update(self[ci].rank); self.num_clause += 1; if learnt { @@ -1157,7 +1156,10 @@ impl ClauseWeaverIF for ClauseDB { ); debug_assert_ne!(next, self.watch[FREE_LIT].next); debug_assert_ne!(0, next.as_ci()); - next.as_ci() + let ci = next.as_ci(); + self.clause[ci].rank = u32::MAX; + self.clause[ci].rank_old = u32::MAX; + ci } } // Check whether a zombi exists