diff --git a/NewDB/src/assignments.rs b/NewDB/src/assignments.rs
index fb937df4..cc393dbf 100644
--- a/NewDB/src/assignments.rs
+++ b/NewDB/src/assignments.rs
@@ -33,7 +33,7 @@ impl ShallowModel for Assignments {
     type ShallowModelTy = Seq<AssignedState>;
 
     #[open]
-#[logic]
+    #[logic]
     fn shallow_model(self) -> Self::ShallowModelTy {
         self.0.shallow_model()
     }
@@ -41,7 +41,7 @@ impl ShallowModel for Assignments {
 
 impl Assignments {
     #[open]
-#[predicate]
+    #[predicate]
     pub fn invariant(self) -> bool {
         pearlite! {
             forall<i: Int> 0 <= i && i < self@.len() ==>
diff --git a/NewDB/src/clause_allocator.rs b/NewDB/src/clause_allocator.rs
index c2f92a59..9b427a57 100644
--- a/NewDB/src/clause_allocator.rs
+++ b/NewDB/src/clause_allocator.rs
@@ -41,7 +41,7 @@ pub(crate) struct ClauseAllocator {
 
 impl ClauseAllocator {
     #[open]
-#[logic]
+    #[logic]
     //#[ensures(forall<i: Int> 0 <= i && i < (self@.buffer).len() ==> (self@.buffer)[i] == (result@.buffer)[i])]
     //#[ensures(result@.num_vars == self.num_vars@)]
     pub(crate) fn push(self, lit: Lit) -> Self {
@@ -49,7 +49,7 @@ impl ClauseAllocator {
     }
 
     #[open]
-#[predicate]
+    #[predicate]
     pub(crate) fn extended(self, new: ClauseAllocator) -> bool {
         pearlite! {
             forall<i: Int> 0 <= i && i < self.buffer@.len() ==> self.buffer@[i] == new.buffer@[i]
@@ -61,13 +61,13 @@ impl ClauseAllocator {
 
 impl ClauseAllocator {
     #[open]
-#[predicate]
+    #[predicate]
     pub(crate) fn invariant(self) -> bool {
         pearlite! { self@.len() <= u32::MAX@ }
     }
 
     #[open]
-#[logic]
+    #[logic]
     //#[requires(cref_invariant(cref, self))]
     pub(crate) fn get_clause_logic(self, cref: Int) -> Seq<Lit> {
         pearlite! {
@@ -76,7 +76,7 @@ impl ClauseAllocator {
     }
 
     #[open]
-#[logic]
+    #[logic]
     //#[requires(cref_invariant(cref, self))]
     pub(crate) fn get_clause_fset(self, cref: Int) -> FSet<Lit> {
         pearlite! {
@@ -85,7 +85,7 @@ impl ClauseAllocator {
     }
 
     #[open]
-#[logic]
+    #[logic]
     //#[requires(cref_invariant(cref, self))]
     #[variant(upper - idx)]
     #[requires(idx >= 0 && upper <= self@.len())]
@@ -106,7 +106,7 @@ impl ShallowModel for ClauseAllocator {
     type ShallowModelTy = Seq<Lit>;
 
     #[open]
-#[logic]
+    #[logic]
     fn shallow_model(self) -> Self::ShallowModelTy {
         self.buffer.shallow_model()
     }
diff --git a/NewDB/src/clause_manager.rs b/NewDB/src/clause_manager.rs
index df16beeb..eeeaf7bb 100644
--- a/NewDB/src/clause_manager.rs
+++ b/NewDB/src/clause_manager.rs
@@ -14,7 +14,7 @@ pub struct ClauseManager {
 
 impl ClauseManager {
     #[open]
-#[predicate]
+    #[predicate]
     pub(crate) fn invariant(self) -> bool {
         pearlite! {
             self.clause_allocator.invariant()
diff --git a/NewDB/src/cref_manager.rs b/NewDB/src/cref_manager.rs
index 5291e774..db498572 100644
--- a/NewDB/src/cref_manager.rs
+++ b/NewDB/src/cref_manager.rs
@@ -16,7 +16,7 @@ impl ShallowModel for CRefManager {
     type ShallowModelTy = Seq<CRef>;
 
     #[open]
-#[logic]
+    #[logic]
     fn shallow_model(self) -> Self::ShallowModelTy {
         self.crefs.shallow_model()
     }
@@ -24,7 +24,7 @@ impl ShallowModel for CRefManager {
 
 impl CRefManager {
     #[open]
-#[predicate]
+    #[predicate]
     pub(crate) fn invariant(self, clause_allocator: ClauseAllocator) -> bool {
         pearlite! {
             clause_allocator.invariant()
@@ -35,7 +35,7 @@ impl CRefManager {
     }
 
     #[open]
-#[predicate]
+    #[predicate]
     pub(crate) fn are_implied_by(self, original_clauses: CRefManager, clause_allocator: ClauseAllocator) -> bool {
         pearlite! {
             let formula = Formula::from(self@, clause_allocator, self.num_vars@);
diff --git a/NewDB/src/formula.rs b/NewDB/src/formula.rs
index 23c99bbf..c76ec139 100644
--- a/NewDB/src/formula.rs
+++ b/NewDB/src/formula.rs
@@ -34,7 +34,7 @@ pub fn abs_just_inner(self, just: Seq<usize>, ix: Int) -> FSet<(theory::Term, th
 impl Formula {
     // TODO: Look at actually implementing from
     #[open]
-#[logic]
+    #[logic]
     #[requires(clause_allocator.invariant())]
     #[requires(forall<i: Int> 0 <= i && i < crefs.len() ==>
                 cref_invariant(crefs[i]@, clause_allocator, num_vars))] // CRefManager.invariant unwrapped -> TODO: refactor?
@@ -46,13 +46,13 @@ impl Formula {
     }
 
     #[open]
-#[logic]
+    #[logic]
     fn insert(self, clause: FSet<Lit>) -> Formula {
         Formula { formula: self.formula.insert(clause), num_vars: self.num_vars }
     }
 
     #[open]
-#[logic]
+    #[logic]
     //#[variant((clause@_allocator).len() - idx)]
     #[variant(crefs.len() - idx)]
     #[requires(idx >= 0)]
@@ -75,7 +75,7 @@ impl Formula {
     }
 
     #[open]
-#[predicate]
+    #[predicate]
     pub(crate) fn implies(self, clause: FSet<Lit>) -> bool {
         pearlite! {
             self.eventually_sat_complete() ==> self.insert(clause).eventually_sat_complete()
@@ -83,7 +83,7 @@ impl Formula {
     }
 
     #[open]
-#[predicate]
+    #[predicate]
     pub(crate) fn eventually_sat_complete(self) -> bool {
         pearlite! {
             exists<a: Seq<AssignedState>> a.len() == self.num_vars
@@ -93,7 +93,7 @@ impl Formula {
     }
 
     #[open]
-#[predicate]
+    #[predicate]
     pub(crate) fn sat(self, a: Seq<AssignedState>) -> bool {
         pearlite! {
             forall<c: _> self.formula.contains(c) ==> clause_sat(c, a)
diff --git a/NewDB/src/friday.rs b/NewDB/src/friday.rs
index b9b35be6..808eb742 100644
--- a/NewDB/src/friday.rs
+++ b/NewDB/src/friday.rs
@@ -14,7 +14,7 @@ struct Pasn {
 
 impl Assignments {
     #[open]
-#[predicate]
+    #[predicate]
     fn compatible(self, pa: Pasn) -> bool {
         pearlite! {
             self.invariant() &&
@@ -31,7 +31,7 @@ pub struct Formula {
 
 impl Formula {
     #[open]
-#[predicate]
+    #[predicate]
     fn invariant(self) -> bool {
         pearlite! {
             forall<i: Int> 0 <= i && i < self.clauses@.len() ==>
@@ -40,7 +40,7 @@ impl Formula {
     }
 
     #[open]
-#[predicate]
+    #[predicate]
     fn sat(self, a: Assignments) -> bool {
         pearlite! {
             forall<i: Int> 0 <= i && i < self.clauses@.len() ==>
@@ -51,7 +51,7 @@ impl Formula {
 
 impl Clause {
     #[open]
-#[predicate]
+    #[predicate]
     fn vars_in_range(self, n: Int) -> bool {
         pearlite! {
             forall<i: Int> 0 <= i && i < self.0@.len() ==>
@@ -62,7 +62,7 @@ impl Clause {
 
 impl Pasn {
     #[open]
-#[predicate]
+    #[predicate]
     fn invariant(self, n: Int) -> bool {
         pearlite! {
             self.ix@ <= self.assign.0@.len()
@@ -74,7 +74,7 @@ impl Pasn {
 
 impl Clause {
     #[open]
-#[predicate]
+    #[predicate]
     fn clause_sat_logic(self, a: Assignments) -> bool {
         pearlite! {
             exists<i: Int> 0 <= i && i < self.0@.len() &&
diff --git a/NewDB/src/lit.rs b/NewDB/src/lit.rs
index 08aa2bdf..2d8ff2ea 100644
--- a/NewDB/src/lit.rs
+++ b/NewDB/src/lit.rs
@@ -13,14 +13,14 @@ pub struct Lit {
 
 impl Lit {
     #[open]
-#[logic]
+    #[logic]
     #[why3::attr = "inline:trivial"]
     pub fn index_logic(self) -> Int {
         pearlite! { self.code@ / 2 }
     }
 
     #[open]
-#[logic]
+    #[logic]
     #[why3::attr = "inline:trivial"]
     pub fn is_positive_logic(self) -> bool {
         pearlite! { self.code@ % 2 == 0 }
@@ -29,7 +29,7 @@ impl Lit {
 
 impl Lit {
     #[open]
-#[predicate]
+    #[predicate]
     pub(crate) fn var_in_range(self, n: Int) -> bool {
         pearlite! {
             self.index_logic() < n
@@ -37,7 +37,7 @@ impl Lit {
     }
 
     #[open]
-#[predicate]
+    #[predicate]
     #[why3::attr = "inline:trivial"]
     pub(crate) fn lit_sat_logic(self, a: Assignments) -> bool {
         pearlite! {
@@ -47,7 +47,7 @@ impl Lit {
 
     // This is the one that is supposed to stay
     #[open]
-#[predicate]
+    #[predicate]
     #[why3::attr = "inline:trivial"]
     pub(crate) fn sat(self, a: Seq<AssignedState>) -> bool {
         pearlite! {
diff --git a/Robinson/src/util.rs b/Robinson/src/util.rs
index d499937f..216bead2 100644
--- a/Robinson/src/util.rs
+++ b/Robinson/src/util.rs
@@ -2,7 +2,7 @@ extern crate creusot_contracts;
 use creusot_contracts::*;
 
 #[predicate]
-#[open]//#[open(self)]
+#[open] //#[open(self)]
 pub fn sorted_range_rev(s: Seq<(usize, usize)>, l: Int, u: Int) -> bool {
     pearlite! {
         forall<i: Int, j: Int> l <= i && i < j && j < u ==> s[i].0 >= s[j].0
@@ -10,7 +10,7 @@ pub fn sorted_range_rev(s: Seq<(usize, usize)>, l: Int, u: Int) -> bool {
 }
 
 #[predicate]
-#[open]//#[open(self)]
+#[open] //#[open(self)]
 pub fn sorted_rev(s: Seq<(usize, usize)>) -> bool {
     sorted_range_rev(s, 0, s.len())
 }