Fix Scratch + remove unneeded parans and proph_consts and the like

CreuSAT/src/assignments.rs

@@ -35,7 +35,7 @@ impl IndexMut<usize> for Assignments {
     #[requires(ix@ < self@.len())]
     #[ensures((*self)@[ix@] == *result)]
     #[ensures((^self)@[ix@] == ^result)]
-    #[ensures(forall<i : Int> 0 <= i && i != ix@ && i < self@.len() ==> self@[i] == (^self)@[i])]
+    #[ensures(forall<i: Int> 0 <= i && i != ix@ && i < self@.len() ==> self@[i] == (^self)@[i])]
     #[ensures((^self)@.len() == (*self)@.len())]
     fn index_mut(&mut self, ix: usize) -> &mut AssignedState {
         #[cfg(not(creusot))]
@@ -67,8 +67,7 @@ impl Assignments {
     #[ensures(long_are_post_unit_inner(_t@, *_f, (^self)@))]
     #[ensures(!unset((^self)@[lit.index_logic()]))]
     #[ensures((^self)@.len() == self@.len())]
-    #[ensures((forall<j : Int> 0 <= j && j < self@.len()
-            && j != lit.index_logic() ==> (*self)@[j] == (^self)@[j]))]
+    #[ensures((forall<j: Int> 0 <= j && j < self@.len() && j != lit.index_logic() ==> self@[j] == (^self)@[j]))]
     #[ensures(lit.sat(^self))]
     pub fn set_assignment(&mut self, lit: Lit, _f: &Formula, _t: &Vec<Step>) {
         let old_self: Ghost<&mut Assignments> = ghost! { self };

CreuSAT/src/clause.rs

@@ -35,9 +35,9 @@ impl IndexMut<usize> for Clause {
     #[inline]
     #[cfg_attr(feature = "trust_clause", trusted)]
     #[requires(ix@ < self@.len())]
-    #[ensures((*self)@[ix@] == *result)]
+    #[ensures(self@[ix@] == *result)]
     #[ensures((^self)@[ix@] == ^result)]
-    #[ensures(forall<i : Int> 0 <= i && i != ix@ && i < self@.len() ==> self@[i] == (^self)@[i])]
+    #[ensures(forall<i: Int> 0 <= i && i != ix@ && i < self@.len() ==> self@[i] == (^self)@[i])]
     #[ensures((^self)@.len() == (*self)@.len())]
     fn index_mut(&mut self, ix: usize) -> &mut Lit {
         #[cfg(not(creusot))]

CreuSAT/src/conflict_analysis.rs

@@ -83,16 +83,11 @@ fn resolve(
     #[invariant(forall<j: Int> 1 <= j && j < i@ ==> o@[j].lit_in(*c))]
     #[invariant(forall<j: Int> 0 <= j && j < old_c@.len()
         && j != c_idx@ ==> old_c@[j].lit_in(*c))]
-    #[invariant((forall<j: Int> 0 <= j && j < c@.len() ==>
-                    (c@[j].lit_in(*old_c.inner()) ||  c@[j].lit_in(*o))))]
+    #[invariant(forall<j: Int> 0 <= j && j < c@.len() ==> (c@[j].lit_in(*old_c.inner()) || c@[j].lit_in(*o)))]
     #[invariant(path_c@ <= c@.len())]
     #[invariant(c.clause_is_seen(*seen))]
     #[invariant(seen@.len() == _f.num_vars@)]
     #[invariant(elems_less_than(to_bump@, _f.num_vars@))]
-    #[invariant(^c == ^old_c.inner())]
-    #[invariant(^seen == ^old_seen.inner())]
-    #[invariant(^path_c == ^old_path_c.inner())]
-    #[invariant(^to_bump == ^old_to_bump.inner())]
     while i < o.len() {
         let old_c3: Ghost<&mut Clause> = ghost!(c);
         proof_assert!(^c == ^old_c3.inner());
@@ -124,8 +119,8 @@ fn resolve(
 #[requires((seen@).len() == _f.num_vars@)]
 #[ensures(match result {
     Some(r) =>  r@ < c@.len()
-                && c@[r@].is_opp((trail.trail@)[(^i)@].lit)
-                && c@[r@].index_logic() == (trail.trail@)[(^i)@].lit.index_logic()
+                && c@[r@].is_opp(trail.trail@[(^i)@].lit)
+                && c@[r@].index_logic() == trail.trail@[(^i)@].lit.index_logic()
                 && (^i)@ < trail.trail@.len()
                 //&& c.same_idx_same_polarity_except(*o, r@)
                 ,
@@ -134,14 +129,12 @@ fn resolve(
 fn choose_literal(c: &Clause, trail: &Trail, i: &mut usize, _f: &Formula, seen: &Vec<bool>) -> Option<usize> {
     let old_i: Ghost<&mut usize> = ghost! {i};
     #[invariant(0 <= i@ && i@ <= trail.trail@.len())]
-    #[invariant(^i == ^old_i.inner())]
     while *i > 0 {
         *i -= 1;
         if seen[trail.trail[*i].lit.index()] {
             let mut k: usize = 0;
             #[invariant(0 <= i@ && i@ < trail.trail@.len())]
             #[invariant(0 <= k@ && k@ <= c@.len())]
-            #[invariant(^i == ^old_i.inner())]
             while k < c.len() {
                 if trail.trail[*i].lit.index() == c[k].index() {
                     return Some(k);
@@ -195,7 +188,7 @@ pub fn analyze_conflict(f: &Formula, trail: &Trail, cref: usize, d: &mut Decisio
     let clause = f[cref].clone();
     let mut j: usize = 0;
     #[invariant(forall<idx: Int> 0 <= idx && idx < seen@.len() ==>
-        (seen@[idx] == (exists<i: Int> 0 <= i && i < j@ && (clause@)[i].index_logic() == idx)))]
+        (seen@[idx] == (exists<i: Int> 0 <= i && i < j@ && clause@[i].index_logic() == idx)))]
     #[invariant(seen@.len() == f.num_vars@)]
     #[invariant(path_c@ <= j@)]
     #[invariant(j@ <= clause@.len())] // This is needed to establish the loop invariant for the next loop
@@ -209,9 +202,8 @@ pub fn analyze_conflict(f: &Formula, trail: &Trail, cref: usize, d: &mut Decisio
         j += 1;
     }
     let mut clause = clause;
-    #[invariant((seen@).len() == f.num_vars@)]
-    #[invariant(forall<idx: Int> 0 <= idx && idx < seen@.len() ==>
-        ((seen@)[idx] == idx_in_logic(idx, clause@)))]
+    #[invariant(seen@.len() == f.num_vars@)]
+    #[invariant(forall<idx: Int> 0 <= idx && idx < seen@.len() ==> (seen@[idx] == idx_in_logic(idx, clause@)))]
     #[invariant(clause.invariant(f.num_vars@))]
     #[invariant(equisat_extension_inner(clause, f@))]
     #[invariant(clause.unsat(trail.assignments))]
@@ -271,9 +263,9 @@ pub fn resolve_empty_clause(f: &Formula, trail: &Trail, cref: usize) -> bool {
     let clause = f[cref].clone();
     let mut to_bump = Vec::new();
     let mut j: usize = 0;
-    #[invariant(forall<idx: Int> 0 <= idx && idx < (seen@).len() ==>
-        ((seen@)[idx] == (exists<i: Int> 0 <= i && i < j@ && (clause@)[i].index_logic() == idx)))]
-    #[invariant((seen@).len() == f.num_vars@)]
+    #[invariant(forall<idx: Int> 0 <= idx && idx < seen@.len() ==>
+        ((seen@)[idx] == (exists<i: Int> 0 <= i && i < j@ && clause@[i].index_logic() == idx)))]
+    #[invariant(seen@.len() == f.num_vars@)]
     #[invariant(j@ <= (clause@).len())]
     // This is needed to establish the loop invariant for the next loop
     while j < clause.len() {

CreuSAT/src/decision.rs

@@ -140,7 +140,6 @@ impl Decisions {
         let mut i: usize = 0;
         let mut curr = self.start;
         #[invariant(curr == usize::MAX || curr@ < self.linked_list@.len())]
-        #[invariant(^old_self.inner() == ^self)]
         #[invariant(forall<j: Int> 0 <= j && j < self.linked_list@.len() ==>
             (self.linked_list@[j].next == old_self.linked_list@[j].next
             && self.linked_list@[j].prev == old_self.linked_list@[j].prev)
@@ -207,7 +206,6 @@ impl Decisions {
         let old_self: Ghost<&mut Decisions> = ghost! { self };
         let mut i: usize = 0;
         #[invariant(old_self.inner() == self)]
-        #[invariant(^old_self.inner() == ^self)]
         #[invariant(v@.len() == counts_with_index@.len())]
         #[invariant(forall<j: Int> 0 <= j && j < i@ ==> counts_with_index@[j].1@ < self.linked_list@.len())]
         while i < v.len() {
@@ -220,7 +218,6 @@ impl Decisions {
         //counts_with_index.sort_unstable_by_key(|k| k.0);
         //counts_with_index.sort_by_key(|k| k.0);
         i = 0;
-        #[invariant(^old_self.inner() == ^self)]
         #[invariant(self.invariant(f.num_vars@))]
         #[invariant(v@.len() == counts_with_index@.len())]
         while i < counts_with_index.len() {

CreuSAT/src/formula.rs

@@ -41,9 +41,9 @@ impl IndexMut<usize> for Formula {
     #[inline]
     #[cfg_attr(feature = "trust_formula", trusted)]
     #[requires(ix@ < self@.0.len())]
-    #[ensures((*self)@.0[ix@] == *result)]
+    #[ensures(self@.0[ix@] == *result)]
     #[ensures((^self)@.0[ix@] == ^result)]
-    #[ensures(forall<i : Int> 0 <= i && i != ix@ && i < self@.0.len() ==> self@.0[i] == (^self)@.0[i])]
+    #[ensures(forall<i: Int> 0 <= i && i != ix@ && i < self@.0.len() ==> self@.0[i] == (^self)@.0[i])]
     #[ensures((^self)@.0.len() == (*self)@.0.len())]
     fn index_mut(&mut self, ix: usize) -> &mut Clause {
         #[cfg(not(creusot))]
@@ -91,12 +91,12 @@ impl Formula {
     #[cfg_attr(feature = "trust_formula", trusted)]
     #[requires(self.invariant())]
     #[requires(a.invariant(*self))]
-    #[requires(idx@ < (self.clauses@).len())]
-    #[ensures(result == (self.clauses@)[idx@].sat(*a))]
+    #[requires(idx@ < self.clauses@.len())]
+    #[ensures(result == self.clauses@[idx@].sat(*a))]
     pub fn is_clause_sat(&self, idx: usize, a: &Assignments) -> bool {
         let clause = &self.clauses[idx];
         let mut i: usize = 0;
-        #[invariant(forall<j: Int> 0 <= j && j < i@ ==> !(clause@)[j].sat(*a))]
+        #[invariant(forall<j: Int> 0 <= j && j < i@ ==> !clause@[j].sat(*a))]
         while i < clause.len() {
             if clause[i].lit_sat(a) {
                 return true;
@@ -118,9 +118,9 @@ impl Formula {
     #[requires(equisat_extension_inner(clause, self@))]
     #[ensures(self.num_vars@ == (^self).num_vars@)]
     #[ensures(self.equisat(^self))]
-    #[ensures(result@ == (self.clauses@).len())]
+    #[ensures(result@ == self.clauses@.len())]
     #[ensures((^self).clauses@[result@] == clause)]
-    #[ensures((self.clauses@).len() + 1 == (^self).clauses@.len())]
+    #[ensures(self.clauses@.len() + 1 == (^self).clauses@.len())]
     pub fn add_clause(&mut self, clause: Clause, watches: &mut Watches, _t: &Trail) -> usize {
         let old_self: Ghost<&mut Formula> = ghost! { self };
         let cref = self.clauses.len();
@@ -144,15 +144,15 @@ impl Formula {
     #[maintains((mut self).invariant())]
     #[maintains(_t.invariant(mut self))]
     #[maintains((mut watches).invariant(mut self))]
-    #[requires((clause@).len() >= 2)]
+    #[requires(clause@.len() >= 2)]
     #[requires(self.num_vars@ < usize::MAX@/2)]
     #[requires(clause.invariant(self.num_vars@))]
     #[requires(equisat_extension_inner(clause, self@))]
     #[ensures(self.num_vars@ == (^self).num_vars@)]
     #[ensures(self.equisat(^self))]
-    #[ensures(result@ == (self.clauses@).len())]
+    #[ensures(result@ == self.clauses@.len())]
     #[ensures((^self).clauses@[result@] == clause)]
-    #[ensures((self.clauses@).len() + 1 == (^self).clauses@.len())]
+    #[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 cref = self.clauses.len();
@@ -171,8 +171,7 @@ impl Formula {
     #[requires(equisat_extension_inner(clause, self@))]
     #[ensures(self.num_vars@ == (^self).num_vars@)]
     //#[ensures(self.equisat_compatible(^self))]
-    #[ensures(forall<i: Int> 0 <= i && i < self.clauses@.len() ==>
-        self.clauses@[i] == (^self).clauses@[i])] // This or equisat_compatible is needed for the watch invariant.
+    #[ensures(forall<i: Int> 0 <= i && i < self.clauses@.len() ==> self.clauses@[i] == (^self).clauses@[i])] // This or equisat_compatible is needed for the watch invariant.
     #[ensures(self.equisat(^self))] // Added/changed
     #[ensures(result@ == self.clauses@.len())]
     #[ensures((^self).clauses@[result@]@.len() == 1)]
@@ -190,7 +189,7 @@ impl Formula {
     #[ensures(result == self.sat(*a))]
     pub fn is_sat(&self, a: &Assignments) -> bool {
         let mut i: usize = 0;
-        #[invariant(forall<k: Int> 0 <= k && k < i@ ==> (self.clauses@)[k].sat(*a))]
+        #[invariant(forall<k: Int> 0 <= k && k < i@ ==> self.clauses@[k].sat(*a))]
         while i < self.clauses.len() {
             if !self.is_clause_sat(i, a) {
                 return false;
@@ -237,8 +236,6 @@ impl Formula {
         #[invariant(watches.invariant(*self))]
         #[invariant(t.invariant(*self))]
         #[invariant(self.invariant())]
-        #[invariant(^watches == ^old_w.inner())]
-        #[invariant(^self == ^old_f.inner())]
         #[invariant(self.num_vars@ == old_f.num_vars@)]
         #[invariant(self.equisat(*old_f.inner()))]
         while i < self.clauses.len() {
@@ -295,8 +292,6 @@ impl Formula {
         #[invariant(watches.invariant(*self))]
         #[invariant(t.invariant(*self))]
         #[invariant(self.invariant())]
-        #[invariant(^watches == ^old_w.inner())]
-        #[invariant(^self == ^old_f.inner())]
         #[invariant(self.num_vars@ == old_f.num_vars@)]
         #[invariant(self.equisat(*old_f.inner()))]
         while i < self.clauses.len() {

CreuSAT/src/lit.rs

@@ -59,7 +59,7 @@ impl Lit {
 
     #[inline(always)]
     #[cfg_attr(feature = "trust_lit", trusted)]
-    #[requires(self.invariant((a@).len()))]
+    #[requires(self.invariant(a@.len()))]
     #[ensures(result == self.sat(*a))]
     pub fn lit_sat(self, a: &Assignments) -> bool {
         match self.is_positive() {
@@ -70,7 +70,7 @@ impl Lit {
 
     #[inline(always)]
     #[cfg_attr(feature = "trust_lit", trusted)]
-    #[requires(self.invariant((a@).len()))]
+    #[requires(self.invariant(a@.len()))]
     #[ensures(result == self.unsat(*a))]
     pub fn lit_unsat(self, a: &Assignments) -> bool {
         match self.is_positive() {
@@ -81,15 +81,15 @@ impl Lit {
 
     #[inline(always)]
     #[cfg_attr(feature = "trust_lit", trusted)]
-    #[requires(self.invariant((a@).len()))]
+    #[requires(self.invariant(a@.len()))]
     #[ensures(result == self.unset(*a))]
     pub fn lit_unset(self, a: &Assignments) -> bool {
         a[self.index()] >= 2
     }
 
     #[inline(always)]
     #[cfg_attr(feature = "trust_lit", trusted)]
-    #[requires(self.invariant((a@).len()))]
+    #[requires(self.invariant(a@.len()))]
     #[ensures(result == !self.unset(*a))]
     pub fn lit_set(self, a: &Assignments) -> bool {
         a[self.index()] < 2

CreuSAT/src/logic/logic_assignments.rs

@@ -46,7 +46,7 @@ impl Assignments {
     pub fn invariant(self, f: Formula) -> bool {
         pearlite! {
             f.num_vars@ == self@.len()
-            && forall<i : Int> 0 <= i && i < self@.len() ==> self@[i]@ <= 3
+            && forall<i: Int> 0 <= i && i < self@.len() ==> self@[i]@ <= 3
         }
     }
 

CreuSAT/src/logic/logic_formula.rs

@@ -36,7 +36,7 @@ pub fn formula_sat_inner(f: (Seq<Clause>, Int), a: Seq<AssignedState>) -> bool {
 #[predicate]
 pub fn eventually_sat_complete(f: (Seq<Clause>, Int)) -> bool {
     pearlite! {
-        exists<a2 : Seq<AssignedState>> a2.len() == f.1 && complete_inner(a2) && formula_sat_inner(f, a2)
+        exists<a2: Seq<AssignedState>> a2.len() == f.1 && complete_inner(a2) && formula_sat_inner(f, a2)
     }
 }
 
@@ -52,7 +52,7 @@ impl Formula {
     #[predicate]
     pub fn eventually_sat_complete(self) -> bool {
         pearlite! {
-            exists<a2 : Seq<AssignedState>> a2.len() == self.num_vars@ && complete_inner(a2) && self.sat_inner(a2)
+            exists<a2: Seq<AssignedState>> a2.len() == self.num_vars@ && complete_inner(a2) && self.sat_inner(a2)
         }
     }
 
@@ -83,14 +83,14 @@ impl Formula {
     #[predicate]
     fn eventually_sat_inner(self, a: Seq<AssignedState>) -> bool {
         pearlite! {
-            exists<a2 : Seq<AssignedState>> a2.len() == self.num_vars@ && compatible_inner(a, a2) && self.sat_inner(a2)
+            exists<a2: Seq<AssignedState>> a2.len() == self.num_vars@ && compatible_inner(a, a2) && self.sat_inner(a2)
         }
     }
 
     #[predicate]
     fn eventually_sat_complete_inner(self, a: Seq<AssignedState>) -> bool {
         pearlite! {
-            exists<a2 : Seq<AssignedState>> a2.len() == self.num_vars@ && compatible_complete_inner(a, a2) && self.sat_inner(a2)
+            exists<a2: Seq<AssignedState>> a2.len() == self.num_vars@ && compatible_complete_inner(a, a2) && self.sat_inner(a2)
         }
     }
 

CreuSAT/src/logic/logic_util.rs

@@ -43,7 +43,7 @@ pub fn partition(v: Seq<(usize, usize)>, i: Int) -> bool {
 
 #[predicate]
 pub fn partition_rev(v: Seq<(usize, usize)>, i: Int) -> bool {
-    pearlite! { forall<k1 : Int, k2: Int> 0 <= k1 && k1 < i && i <= k2 && k2 < v.len() ==> v[k1].0 >= v[k2].0 }
+    pearlite! { forall<k1: Int, k2: Int> 0 <= k1 && k1 < i && i <= k2 && k2 < v.len() ==> v[k1].0 >= v[k2].0 }
 }
 
 #[predicate]

CreuSAT/src/logic/logic_watches.rs

@@ -24,7 +24,7 @@ pub fn watches_invariant_internal(w: Seq<Vec<Watcher>>, n: Int, f: Formula) -> b
 #[predicate]
 pub fn watch_valid(w: Seq<Watcher>, f: Formula) -> bool {
     pearlite! {
-        forall<j : Int> 0 <= j && j < w.len() ==>
+        forall<j: Int> 0 <= j && j < w.len() ==>
                 w[j].cref@ < f.clauses@.len() // all clauses are valid
             &&  f.clauses@[w[j].cref@]@.len() > 1 // the clauses have at least two litearls
             && w[j].blocker.index_logic() < f.num_vars@ // something about blocking lits

CreuSAT/src/solver.rs

@@ -237,10 +237,6 @@ impl Solver {
         #[invariant(d.invariant(f.num_vars@))]
         #[invariant(old_f.inner().equisat(*f))]
         #[invariant(f.num_vars@ == old_f.num_vars@)]
-        #[invariant(^f == ^old_f.inner())]
-        #[invariant(^t == ^old_t.inner())]
-        #[invariant(^w == ^old_w.inner())]
-        #[invariant(^d == ^old_d.inner())]
         loop {
             match self.unit_prop_step(f, d, t, w) {
                 ConflictResult::Ok => {
@@ -331,7 +327,6 @@ impl Solver {
         #[invariant(trail.invariant(*formula))]
         #[invariant(watches.invariant(*formula))]
         #[invariant(decisions.invariant(formula.num_vars@))]
-        #[invariant(^formula == ^old_f.inner())]
         loop {
             match self.outer_loop(formula, &mut decisions, &mut trail, &mut watches) {
                 SatResult::Unknown => {} // continue

CreuSAT/src/trail.rs

@@ -129,8 +129,6 @@ impl Trail {
         #[invariant(self.invariant_no_decision(*f))]
         #[invariant(d.invariant(f.num_vars@))]
         //#[invariant((self@.trail).len() == old_t.trail@.len() - i@)] // we don't care anymore
-        #[invariant(^old_t.inner() == ^self)]
-        #[invariant(^old_d.inner() == ^d)]
         #[invariant(curr@ < d.linked_list@.len() || curr@ == usize::MAX@)]
         // Hmm maybe change invariant
         while i < how_many {
@@ -147,7 +145,6 @@ impl Trail {
 
         #[invariant(long_are_post_unit_inner(self.trail@, *f, self.assignments@))]
         #[invariant(self.invariant_no_decision(*f))]
-        #[invariant(^old_t.inner() == ^self)]
         while self.decisions.len() > level {
             let old_t2: Ghost<&mut Trail> = ghost! { self };
             proof_assert!(sorted(self.decisions@));
@@ -167,7 +164,6 @@ impl Trail {
         // This is a noop, and should be proven away.
         #[invariant(long_are_post_unit_inner(self.trail@, *f, self.assignments@))]
         #[invariant(self.invariant_no_decision(*f))]
-        #[invariant(^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 };
             proof_assert!(sorted(self.decisions@));
@@ -225,7 +221,7 @@ impl Trail {
     #[requires(!step.lit.idx_in_trail(self.trail))]
     #[requires(unset(self.assignments@[step.lit.index_logic()]))] // Should not be needed anymore
     #[requires(long_are_post_unit_inner(self.trail@, *_f, self.assignments@))]
-    #[ensures((forall<j : Int> 0 <= j && j < self.assignments@.len() &&
+    #[ensures((forall<j: Int> 0 <= j && j < self.assignments@.len() &&
         j != step.lit.index_logic() ==> self.assignments@[j] == (^self).assignments@[j]))]
     #[ensures(step.lit.sat((^self).assignments))]
     #[ensures(long_are_post_unit_inner((^self).trail@, *_f, (^self).assignments@))]
@@ -256,7 +252,7 @@ impl Trail {
     #[maintains((mut self).invariant(*_f))]
     #[requires(idx@ < _f.num_vars@)]
     #[requires(unset(self.assignments@[idx@]))]
-    #[ensures((forall<j : Int> 0 <= j && j < self.assignments@.len() &&
+    #[ensures((forall<j: Int> 0 <= j && j < self.assignments@.len() &&
         j != idx@ ==> self.assignments@[j] == (^self).assignments@[j]))]
     #[ensures((^self).assignments@[idx@]@ == 1 || (^self).assignments@[idx@]@ == 0)] // Is this needed?
     #[requires(long_are_post_unit_inner(self.trail@, *_f, self.assignments@))]
@@ -316,8 +312,6 @@ impl Trail {
         let old_d: Ghost<&mut Decisions> = ghost! { d };
         let old_self: Ghost<&mut Trail> = ghost! { self };
         #[invariant(self.invariant(*f))]
-        #[invariant(^old_self.inner() == ^self)]
-        #[invariant(^old_d.inner() == ^d)]
         #[invariant(d.invariant(f.num_vars@))]
         while i < f.clauses.len() {
             let clause = &f[i];