Update Replay + cargo fmt.

.github/workflows/replay.yml

@@ -52,5 +52,5 @@ jobs:
     - name: Replay
       run: |
         eval $(opam env)
-        WHY3CONFIG= why3 replay -Lprelude --obsolete-only mlcfgs/CreuSAT
+        WHY3CONFIG= why3 replay -Lprelude --merging-only mlcfgs/CreuSAT
 

CreuSAT/src/decision.rs

@@ -134,7 +134,7 @@ impl Decisions {
     #[ensures((@(^self).linked_list).len() == (@self.linked_list).len())]
     fn rescore(&mut self, _f: &Formula) {
         let INVALID: usize = usize::MAX;
-        let old_self : Ghost<&mut Decisions>= ghost! { self };
+        let old_self: Ghost<&mut Decisions> = ghost! { self };
         let mut curr_score = self.linked_list.len();
         let mut i: usize = 0;
         let mut curr = self.start;

CreuSAT/src/formula.rs

@@ -156,7 +156,7 @@ impl Formula {
     #[ensures((@(^self).clauses)[@result] == clause)]
     #[ensures((@self.clauses).len() + 1 == (@(^self).clauses).len())]
     pub fn add_unwatched_clause(&mut self, clause: Clause, watches: &mut Watches, _t: &Trail) -> usize {
-        let old_self: Ghost<&mut Formula>= ghost! { self };
+        let old_self: Ghost<&mut Formula> = ghost! { self };
         let cref = self.clauses.len();
         self.clauses.push(clause);
         proof_assert!(old_self.equisat_compatible(*self));

CreuSAT/src/trail.rs

@@ -172,7 +172,7 @@ impl Trail {
         #[invariant(inv, self.invariant_no_decision(*f))]
         #[invariant(proph, ^old_t.inner() == ^self)]
         while self.decisions.len() > 0 && self.decisions[self.decisions.len() - 1] > self.trail.len() {
-            let old_t3: Ghost<& mut Trail> = ghost! { self };
+            let old_t3: Ghost<&mut Trail> = ghost! { self };
             proof_assert!(sorted(@self.decisions));
             proof_assert!((@self.decisions).len() > 0);
             proof_assert!(lemma_pop_maintains_sorted(@self.decisions); true);

CreuSAT/src/unit_prop.rs

@@ -4,7 +4,7 @@ use creusot_contracts::logic::Ghost;
 use creusot_contracts::std::*;
 use creusot_contracts::*;
 
-use crate::{formula::*, lit::*, trail::*, util, watches::*, clause::*};
+use crate::{clause::*, formula::*, lit::*, trail::*, util, watches::*};
 
 use crate::logic::{
     logic::*,

Makefile.toml

@@ -75,7 +75,7 @@ dependencies = [
 [tasks.creusot-CreuSAT]
 workspace = false
 command = "cargo"
-args = ["creusot", "--", "-p", "CreuSAT", "--features=contracts", "--features", "${@}"]
+args = ["creusot", "--span-mode=relative", "--", "-p", "CreuSAT", "--features=contracts", "--features", "${@}"]
 
 [tasks.move-CreuSAT]
 workspace = false

mlcfgs/CreuSAT.mlcfg

@@ -12490,7 +12490,7 @@ module CreuSat_Formula_Impl2_AddUnwatchedClause
   }
   BB4 {
     _6 <- ();
-    old_self_5 <- ghost ([#"../CreuSAT/src/formula.rs" 159 43 159 58] self_1);
+    old_self_5 <- ghost ([#"../CreuSAT/src/formula.rs" 159 44 159 59] self_1);
     goto BB5
   }
   BB5 {
@@ -17580,7 +17580,7 @@ module CreuSat_Trail_Impl0_BacktrackTo
   }
   BB35 {
     _88 <- ();
-    old_t3_87 <- ghost ([#"../CreuSAT/src/trail.rs" 175 45 175 60] self_1);
+    old_t3_87 <- ghost ([#"../CreuSAT/src/trail.rs" 175 44 175 59] self_1);
     goto BB36
   }
   BB36 {