Bump Clap version. Ghost to Snapshot in Scratch and NewDB

NewDB/src/clause_allocator.rs

@@ -131,7 +131,7 @@ impl ClauseAllocator {
         let cref = self.buffer.len() as CRef;
         self.buffer.push(Lit::raw(lits.len() as u32));
 
-        let old_self: Ghost<&mut ClauseAllocator> = ghost!(self);
+        let old_self: Snapshot<&mut ClauseAllocator> = snapshot!(self);
 
         #[invariant(self.num_vars == old_self.num_vars)] // TODO: Don't like this
         #[invariant(^*old_self == ^self)]

NewDB/src/clause_manager.rs

@@ -68,7 +68,7 @@ impl ClauseManager {
     //#[requires([email protected]() + (@lits).len() + @HEADER_LEN <= @u32::MAX)] // TODO: May have to move this to a runtime check
     #[requires(clause_invariant_seq(lits@, self.clause_allocator.num_vars@))]
     pub(crate) fn learn_clause(&mut self, lits: &[Lit]) -> CRef {
-        let old_self: Ghost<&mut ClauseManager> = ghost!(self);
+        let old_self: Snapshot<&mut ClauseManager> = snapshot!(self);
         proof_assert!(self.learnt_core.are_implied_by(self.original_clauses, self.clause_allocator));
         let cref = self.clause_allocator.add_clause(lits);
         proof_assert!(^*old_self == ^self);

Scratch/Cargo.toml

@@ -5,7 +5,7 @@ authors = ["Sarek Høverstad Skotåm <[email protected]>"]
 edition = "2021"
 
 [dependencies]
-clap = "2.33.3"
+clap = "4.5.4"
 creusot-contracts = { git = "https://github.com/xldenis/creusot", version = "^0", rev = "1357cc97" }
 
 # This is just copied verbatim from CreuSAT.

Scratch/src/clause.rs

@@ -1,5 +1,5 @@
 extern crate creusot_contracts;
-use creusot_contracts::{std::*, Clone, Ghost, *};
+use creusot_contracts::{std::*, Clone, Snapshot, *};
 
 use crate::{assignments::*, formula::*, lit::*};
 

Scratch/src/scratch.rs

@@ -44,7 +44,7 @@ pub fn lemma_clause_permuted_maintains_unsat(c: Clause, a: Assignments) {}
 #[ensures(f.clauses@.len() == (^f).clauses@.len())]
 #[ensures(f.equisat(^f))] // This one is hard (both ways equisat)
 fn swap(f: &mut Formula, cref: usize, j: usize, k: usize, assignments: Assignments) {
-    let old_f: Ghost<&mut Formula> = ghost! { f };
+    let old_f: Snapshot<&mut Formula> = snapshot! { f };
 
     f.clauses[cref].lits.swap(j, k);