diff --git a/cargo-creusot/src/options.rs b/cargo-creusot/src/options.rs
index e4a7897a78..0fa2cb17f6 100644
--- a/cargo-creusot/src/options.rs
+++ b/cargo-creusot/src/options.rs
@@ -32,6 +32,9 @@ pub struct CreusotArgs {
     /// Check the installed why3 version.
     #[clap(long, default_value_t = true, action = clap::ArgAction::Set)]
     pub check_why3: bool,
+    /// Use `result` as the trigger of definition and specification axioms of logic/ghost/predicate functions
+    #[clap(long, default_value_t = false, action = clap::ArgAction::Set)]
+    pub simple_triggers: bool,
 }
 
 /// Parse a single key-value pair
diff --git a/creusot-contracts-proc/src/lib.rs b/creusot-contracts-proc/src/lib.rs
index a9dea895cd..9a4cc1b018 100644
--- a/creusot-contracts-proc/src/lib.rs
+++ b/creusot-contracts-proc/src/lib.rs
@@ -543,7 +543,8 @@ pub fn law(_: TS1, tokens: TS1) -> TS1 {
     let tokens = TokenStream::from(tokens);
     TS1::from(quote! {
         #[creusot::decl::law]
-        #[::creusot_contracts::ghost]
+        #[creusot::decl::no_trigger]
+        #[::creusot_contracts::logic]
         #tokens
     })
 }
diff --git a/creusot-contracts/src/logic.rs b/creusot-contracts/src/logic.rs
index 568ed21121..7d66d19075 100644
--- a/creusot-contracts/src/logic.rs
+++ b/creusot-contracts/src/logic.rs
@@ -5,7 +5,7 @@ mod fset;
 mod int;
 mod mapping;
 mod ops;
-mod ord;
+pub mod ord;
 mod seq;
 mod set;
 
diff --git a/creusot-contracts/src/logic/ord.rs b/creusot-contracts/src/logic/ord.rs
index 7a4c223db6..e5f9177019 100644
--- a/creusot-contracts/src/logic/ord.rs
+++ b/creusot-contracts/src/logic/ord.rs
@@ -70,6 +70,67 @@ pub trait OrdLogic {
     fn eq_cmp(x: Self, y: Self);
 }
 
+#[macro_export]
+macro_rules! ord_laws_impl {
+    () => {
+        #[::creusot_contracts::law]
+        #[::creusot_contracts::open(self)]
+        fn cmp_le_log(_: Self, _: Self) {
+            ()
+        }
+
+        #[::creusot_contracts::law]
+        #[::creusot_contracts::open(self)]
+        fn cmp_lt_log(_: Self, _: Self) {
+            ()
+        }
+
+        #[::creusot_contracts::law]
+        #[::creusot_contracts::open(self)]
+        fn cmp_ge_log(_: Self, _: Self) {
+            ()
+        }
+
+        #[::creusot_contracts::law]
+        #[::creusot_contracts::open(self)]
+        fn cmp_gt_log(_: Self, _: Self) {
+            ()
+        }
+
+        #[::creusot_contracts::law]
+        #[::creusot_contracts::open(self)]
+        fn refl(_: Self) {
+            ()
+        }
+
+        #[::creusot_contracts::law]
+        #[::creusot_contracts::open(self)]
+        fn trans(_: Self, _: Self, _: Self, _: Ordering) {
+            ()
+        }
+
+        #[::creusot_contracts::law]
+        #[::creusot_contracts::open(self)]
+        fn antisym1(_: Self, _: Self) {
+            ()
+        }
+
+        #[::creusot_contracts::law]
+        #[::creusot_contracts::open(self)]
+        fn antisym2(_: Self, _: Self) {
+            ()
+        }
+
+        #[::creusot_contracts::law]
+        #[::creusot_contracts::open(self)]
+        fn eq_cmp(_: Self, _: Self) {
+            ()
+        }
+    };
+}
+
+pub use ord_laws_impl;
+
 macro_rules! ord_logic_impl {
     ($t:ty) => {
         impl OrdLogic for $t {
@@ -117,59 +178,7 @@ macro_rules! ord_logic_impl {
                 true
             }
 
-            #[ghost]
-            #[open(self)]
-            fn cmp_le_log(_: Self, _: Self) {
-                ()
-            }
-
-            #[ghost]
-            #[open(self)]
-            fn cmp_lt_log(_: Self, _: Self) {
-                ()
-            }
-
-            #[ghost]
-            #[open(self)]
-            fn cmp_ge_log(_: Self, _: Self) {
-                ()
-            }
-
-            #[ghost]
-            #[open(self)]
-            fn cmp_gt_log(_: Self, _: Self) {
-                ()
-            }
-
-            #[ghost]
-            #[open(self)]
-            fn refl(_: Self) {
-                ()
-            }
-
-            #[ghost]
-            #[open(self)]
-            fn trans(_: Self, _: Self, _: Self, _: Ordering) {
-                ()
-            }
-
-            #[ghost]
-            #[open(self)]
-            fn antisym1(_: Self, _: Self) {
-                ()
-            }
-
-            #[ghost]
-            #[open(self)]
-            fn antisym2(_: Self, _: Self) {
-                ()
-            }
-
-            #[ghost]
-            #[open(self)]
-            fn eq_cmp(_: Self, _: Self) {
-                ()
-            }
+            ord_laws_impl! {}
         }
     };
 }
@@ -202,41 +211,7 @@ impl OrdLogic for bool {
         }
     }
 
-    #[ghost]
-    #[open(self)]
-    fn cmp_le_log(_: Self, _: Self) {}
-
-    #[ghost]
-    #[open(self)]
-    fn cmp_lt_log(_: Self, _: Self) {}
-
-    #[ghost]
-    #[open(self)]
-    fn cmp_ge_log(_: Self, _: Self) {}
-
-    #[ghost]
-    #[open(self)]
-    fn cmp_gt_log(_: Self, _: Self) {}
-
-    #[ghost]
-    #[open(self)]
-    fn refl(_: Self) {}
-
-    #[ghost]
-    #[open(self)]
-    fn trans(_: Self, _: Self, _: Self, _: Ordering) {}
-
-    #[ghost]
-    #[open(self)]
-    fn antisym1(_: Self, _: Self) {}
-
-    #[ghost]
-    #[open(self)]
-    fn antisym2(_: Self, _: Self) {}
-
-    #[ghost]
-    #[open(self)]
-    fn eq_cmp(_: Self, _: Self) {}
+    ord_laws_impl! {}
 }
 
 impl<A: OrdLogic, B: OrdLogic> OrdLogic for (A, B) {
@@ -259,59 +234,25 @@ impl<A: OrdLogic, B: OrdLogic> OrdLogic for (A, B) {
         pearlite! { (self.0 == o.0 && self.1 <= o.1) || self.0 <= o.0 }
     }
 
-    #[ghost]
-    #[open(self)]
-    fn cmp_le_log(_: Self, _: Self) {}
-
     #[ghost]
     #[open]
     fn lt_log(self, o: Self) -> bool {
         pearlite! { (self.0 == o.0 && self.1 < o.1) || self.0 < o.0 }
     }
 
-    #[ghost]
-    #[open(self)]
-    fn cmp_lt_log(_: Self, _: Self) {}
-
     #[ghost]
     #[open]
     fn ge_log(self, o: Self) -> bool {
         pearlite! { (self.0 == o.0 && self.1 >= o.1) || self.0 >= o.0 }
     }
 
-    #[ghost]
-    #[open(self)]
-    fn cmp_ge_log(_: Self, _: Self) {}
-
     #[ghost]
     #[open]
     fn gt_log(self, o: Self) -> bool {
         pearlite! { (self.0 == o.0 && self.1 > o.1) || self.0 > o.0 }
     }
 
-    #[ghost]
-    #[open(self)]
-    fn cmp_gt_log(_: Self, _: Self) {}
-
-    #[ghost]
-    #[open(self)]
-    fn refl(_: Self) {}
-
-    #[ghost]
-    #[open(self)]
-    fn trans(_: Self, _: Self, _: Self, _: Ordering) {}
-
-    #[ghost]
-    #[open(self)]
-    fn antisym1(_: Self, _: Self) {}
-
-    #[ghost]
-    #[open(self)]
-    fn antisym2(_: Self, _: Self) {}
-
-    #[ghost]
-    #[open(self)]
-    fn eq_cmp(_: Self, _: Self) {}
+    ord_laws_impl! {}
 }
 
 impl<T: OrdLogic> OrdLogic for Option<T> {
@@ -326,52 +267,5 @@ impl<T: OrdLogic> OrdLogic for Option<T> {
         }
     }
 
-    #[law]
-    #[open(self)]
-    #[ensures(x.le_log(y) == (x.cmp_log(y) != Ordering::Greater))]
-    fn cmp_le_log(x: Self, y: Self) {}
-
-    #[law]
-    #[open(self)]
-    #[ensures(x.lt_log(y) == (x.cmp_log(y) == Ordering::Less))]
-    fn cmp_lt_log(x: Self, y: Self) {}
-
-    #[law]
-    #[open(self)]
-    #[ensures(x.ge_log(y) == (x.cmp_log(y) != Ordering::Less))]
-    fn cmp_ge_log(x: Self, y: Self) {}
-
-    #[law]
-    #[open(self)]
-    #[ensures(x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater))]
-    fn cmp_gt_log(x: Self, y: Self) {}
-
-    #[law]
-    #[open(self)]
-    #[ensures(x.cmp_log(x) == Ordering::Equal)]
-    fn refl(x: Self) {}
-
-    #[law]
-    #[open(self)]
-    #[requires(x.cmp_log(y) == o)]
-    #[requires(y.cmp_log(z) == o)]
-    #[ensures(x.cmp_log(z) == o)]
-    fn trans(x: Self, y: Self, z: Self, o: Ordering) {}
-
-    #[law]
-    #[open(self)]
-    #[requires(x.cmp_log(y) == Ordering::Less)]
-    #[ensures(y.cmp_log(x) == Ordering::Greater)]
-    fn antisym1(x: Self, y: Self) {}
-
-    #[law]
-    #[open(self)]
-    #[requires(x.cmp_log(y) == Ordering::Greater)]
-    #[ensures(y.cmp_log(x) == Ordering::Less)]
-    fn antisym2(x: Self, y: Self) {}
-
-    #[law]
-    #[open(self)]
-    #[ensures((x == y) == (x.cmp_log(y) == Ordering::Equal))]
-    fn eq_cmp(x: Self, y: Self) {}
+    ord_laws_impl! {}
 }
diff --git a/creusot-contracts/src/num_rational.rs b/creusot-contracts/src/num_rational.rs
index 8593cd2d86..f6a50878fa 100644
--- a/creusot-contracts/src/num_rational.rs
+++ b/creusot-contracts/src/num_rational.rs
@@ -65,57 +65,5 @@ impl OrdLogic for Real {
         true
     }
 
-    #[ghost]
-    #[open(self)]
-    fn cmp_le_log(_: Self, _: Self) {
-        ()
-    }
-
-    #[ghost]
-    #[open(self)]
-    fn cmp_lt_log(_: Self, _: Self) {
-        ()
-    }
-
-    #[ghost]
-    #[open(self)]
-    fn cmp_ge_log(_: Self, _: Self) {
-        ()
-    }
-
-    #[ghost]
-    #[open(self)]
-    fn cmp_gt_log(_: Self, _: Self) {
-        ()
-    }
-
-    #[ghost]
-    #[open(self)]
-    fn refl(_: Self) {
-        ()
-    }
-
-    #[ghost]
-    #[open(self)]
-    fn trans(_: Self, _: Self, _: Self, _: Ordering) {
-        ()
-    }
-
-    #[ghost]
-    #[open(self)]
-    fn antisym1(_: Self, _: Self) {
-        ()
-    }
-
-    #[ghost]
-    #[open(self)]
-    fn antisym2(_: Self, _: Self) {
-        ()
-    }
-
-    #[ghost]
-    #[open(self)]
-    fn eq_cmp(_: Self, _: Self) {
-        ()
-    }
+    crate::logic::ord::ord_laws_impl! {}
 }
diff --git a/creusot-rustc/src/options.rs b/creusot-rustc/src/options.rs
index b97e4ab7a1..30511b8116 100644
--- a/creusot-rustc/src/options.rs
+++ b/creusot-rustc/src/options.rs
@@ -35,6 +35,9 @@ pub struct CreusotArgs {
     /// Check the installed why3 version.
     #[clap(long, default_value_t = true, action = clap::ArgAction::Set)]
     pub check_why3: bool,
+    /// uses `result` as the trigger of definition and specification axioms of logic/ghost/predicate functions
+    #[clap(long, default_value_t = false, action = clap::ArgAction::Set)]
+    pub simple_triggers: bool,
 }
 
 /// Parse a single key-value pair
@@ -93,6 +96,7 @@ impl CreusotArgs {
             in_cargo: cargo_creusot,
             span_mode: span_mode,
             match_str: self.focus_on,
+            simple_triggers: self.simple_triggers,
         }
     }
 }
diff --git a/creusot/src/backend/logic.rs b/creusot/src/backend/logic.rs
index 5cfa3b152a..642965da4a 100644
--- a/creusot/src/backend/logic.rs
+++ b/creusot/src/backend/logic.rs
@@ -9,7 +9,7 @@ use crate::{
 use rustc_hir::def_id::DefId;
 use why3::{
     declaration::*,
-    exp::{BinOp, Binder, Exp},
+    exp::{BinOp, Binder, Exp, Trigger},
     Ident, QName,
 };
 
@@ -269,7 +269,8 @@ pub(crate) fn spec_axiom(sig: &Signature) -> Axiom {
     let mut condition = preconditions.rfold(postcondition, |acc, arg| arg.implies(acc));
 
     let func_call = function_call(sig);
-    condition.subst(&[("result".into(), func_call)].into_iter().collect());
+    let trigger = sig.trigger.clone().unwrap_or_else(|| Trigger::single(func_call.clone()));
+    condition.subst(&[("result".into(), func_call.clone())].into_iter().collect());
     let args: Vec<(_, _)> = sig
         .args
         .iter()
@@ -278,7 +279,8 @@ pub(crate) fn spec_axiom(sig: &Signature) -> Axiom {
         .filter(|arg| &*arg.0 != "_")
         .collect();
 
-    let axiom = if args.is_empty() { condition } else { Exp::Forall(args, Box::new(condition)) };
+    let axiom =
+        if args.is_empty() { condition } else { Exp::forall_trig(args, trigger, condition) };
 
     Axiom { name: format!("{}_spec", &*sig.name).into(), rewrite: false, axiom }
 }
@@ -301,15 +303,17 @@ fn function_call(sig: &Signature) -> Exp {
 
 fn definition_axiom(sig: &Signature, body: Exp) -> Axiom {
     let call = function_call(sig);
+    let trigger = sig.trigger.clone().unwrap_or_else(|| Trigger::single(call.clone()));
 
-    let equation = Exp::BinaryOp(BinOp::Eq, Box::new(call), Box::new(body));
+    let equation = Exp::BinaryOp(BinOp::Eq, Box::new(call.clone()), Box::new(body));
 
     let preconditions = sig.contract.requires.iter().cloned();
     let condition = preconditions.rfold(equation, |acc, arg| arg.implies(acc));
 
     let args: Vec<_> = sig.args.clone().into_iter().flat_map(|b| b.var_type_pairs()).collect();
 
-    let axiom = if args.is_empty() { condition } else { Exp::Forall(args, Box::new(condition)) };
+    let axiom =
+        if args.is_empty() { condition } else { Exp::forall_trig(args, trigger, condition) };
 
     Axiom { name: "def".into(), rewrite: false, axiom }
 }
diff --git a/creusot/src/backend/signature.rs b/creusot/src/backend/signature.rs
index 30d83a8b8a..723f864982 100644
--- a/creusot/src/backend/signature.rs
+++ b/creusot/src/backend/signature.rs
@@ -1,14 +1,17 @@
 use rustc_hir::{def::Namespace, def_id::DefId};
 use why3::{
     declaration::{Contract, Signature},
-    exp::Binder,
+    exp::{Binder, Trigger},
+    ty::Type,
 };
 
 use crate::{
     backend,
     ctx::CloneMap,
     translation::specification::PreContract,
-    util::{ident_of, item_name, why3_attrs, AnonymousParamName, PreSignature},
+    util::{
+        ident_of, item_name, should_replace_trigger, why3_attrs, AnonymousParamName, PreSignature,
+    },
 };
 
 use super::{term::lower_pure, Why3Generator};
@@ -63,7 +66,15 @@ pub(crate) fn sig_to_why3<'tcx>(
 
     let retty = names
         .with_public_clones(|names| backend::ty::translate_ty(ctx, names, span, pre_sig.output));
-    Signature { name, attrs, retty: Some(retty), args, contract }
+    let trigger = if ctx.opts.simple_triggers
+        && should_replace_trigger(ctx.tcx, def_id)
+        && retty != Type::UNIT
+    {
+        None
+    } else {
+        Some(Trigger::NONE)
+    };
+    Signature { name, trigger, attrs, retty: Some(retty), args, contract }
 }
 
 fn contract_to_why3<'tcx>(
diff --git a/creusot/src/backend/term.rs b/creusot/src/backend/term.rs
index 9c3a4f1f29..63759b1b67 100644
--- a/creusot/src/backend/term.rs
+++ b/creusot/src/backend/term.rs
@@ -151,19 +151,13 @@ impl<'tcx> Lower<'_, 'tcx> {
             TermKind::Forall { binder, box body } => {
                 let ty = translate_ty(self.ctx, self.names, rustc_span::DUMMY_SP, binder.1);
                 self.pure_exp(|this| {
-                    Exp::Forall(
-                        vec![(binder.0.to_string().into(), ty)],
-                        Box::new(this.lower_term(body)),
-                    )
+                    Exp::forall(vec![(binder.0.to_string().into(), ty)], this.lower_term(body))
                 })
             }
             TermKind::Exists { binder, box body } => {
                 let ty = translate_ty(self.ctx, self.names, rustc_span::DUMMY_SP, binder.1);
                 self.pure_exp(|this| {
-                    Exp::Exists(
-                        vec![(binder.0.to_string().into(), ty)],
-                        Box::new(this.lower_term(body)),
-                    )
+                    Exp::exists(vec![(binder.0.to_string().into(), ty)], this.lower_term(body))
                 })
             }
             TermKind::Constructor { typ, variant, fields } => {
diff --git a/creusot/src/backend/ty.rs b/creusot/src/backend/ty.rs
index 0f5f494cfb..9a280e22f1 100644
--- a/creusot/src/backend/ty.rs
+++ b/creusot/src/backend/ty.rs
@@ -23,7 +23,7 @@ use why3::{
         AdtDecl, ConstructorDecl, Contract, Decl, Field, LetDecl, LetKind, Module, Signature,
         TyDecl, Use,
     },
-    exp::{Binder, Exp, Pattern},
+    exp::{Binder, Exp, Pattern, Trigger},
     ty::Type as MlT,
     Ident, QName,
 };
@@ -499,6 +499,7 @@ pub(crate) fn translate_accessor(
         variant_ix.into(),
         &variant_arities,
         (ix, target_ty, false),
+        &ctx.ctx,
     )
 }
 
@@ -508,12 +509,16 @@ pub(crate) fn build_accessor(
     variant_ix: usize,
     variant_arities: &[(QName, usize)],
     target_field: (usize, MlT, bool),
+    ctx: &TranslationCtx<'_>,
 ) -> Decl {
     let field_ty = target_field.1;
     let field_ix = target_field.0;
 
+    let trigger = if ctx.opts.simple_triggers { None } else { Some(Trigger::NONE) };
+
     let sig = Signature {
         name: acc_name.clone(),
+        trigger,
         attrs: Vec::new(),
         args: vec![Binder::typed("self".into(), this.clone())],
         retty: Some(field_ty.clone()),
diff --git a/creusot/src/backend/ty_inv.rs b/creusot/src/backend/ty_inv.rs
index d17d8cb469..2d6337b2bd 100644
--- a/creusot/src/backend/ty_inv.rs
+++ b/creusot/src/backend/ty_inv.rs
@@ -11,7 +11,7 @@ use rustc_middle::ty::{subst::SubstsRef, AdtDef, GenericArg, ParamEnv, Ty, TyCtx
 use rustc_span::{Symbol, DUMMY_SP};
 use why3::{
     declaration::{Axiom, Decl, Module, TyDecl},
-    exp::{Constant, Exp, Pattern},
+    exp::{Constant, Exp, Pattern, Trigger},
     ty::Type as MlT,
     Ident, QName,
 };
@@ -187,10 +187,13 @@ fn build_inv_axiom<'tcx>(
             .unwrap_or_else(|| Exp::mk_true())
     };
     let trivial = rhs.is_true();
+    let trigger =
+        if ctx.opts.simple_triggers { Trigger::single(lhs.clone()) } else { Trigger::NONE };
 
-    let axiom = Exp::Forall(
+    let axiom = Exp::forall_trig(
         vec![("self".into(), translate_ty(ctx, names, DUMMY_SP, ty))],
-        Box::new(lhs.eq(rhs)),
+        trigger,
+        lhs.eq(rhs),
     );
     Axiom { name, rewrite: !trivial, axiom }
 }
@@ -333,7 +336,7 @@ fn build_inv_exp_seq<'tcx>(
     let mut body = build_inv_exp(ctx, names, "a".into(), ty, param_env, Mode::Field)?;
     body.subst(&[("a".into(), ith)].into());
 
-    Some(Exp::Forall(vec![("i".into(), MlT::Integer)], Box::new(bounds.implies(body))))
+    Some(Exp::forall(vec![("i".into(), MlT::Integer)], bounds.implies(body)))
 }
 
 fn build_inv_exp_adt<'tcx>(
diff --git a/creusot/src/options.rs b/creusot/src/options.rs
index 6ef1690560..1b36a9415c 100644
--- a/creusot/src/options.rs
+++ b/creusot/src/options.rs
@@ -20,6 +20,7 @@ pub struct Options {
     pub in_cargo: bool,
     pub span_mode: SpanMode,
     pub match_str: Option<String>,
+    pub simple_triggers: bool,
 }
 
 #[derive(Debug, Clone)]
diff --git a/creusot/src/util.rs b/creusot/src/util.rs
index 0a144afc1b..c3362ce1ad 100644
--- a/creusot/src/util.rs
+++ b/creusot/src/util.rs
@@ -104,6 +104,10 @@ pub(crate) fn is_law(tcx: TyCtxt, def_id: DefId) -> bool {
     get_attr(tcx.get_attrs_unchecked(def_id), &["creusot", "decl", "law"]).is_some()
 }
 
+pub(crate) fn should_replace_trigger(tcx: TyCtxt, def_id: DefId) -> bool {
+    get_attr(tcx.get_attrs_unchecked(def_id), &["creusot", "decl", "no_trigger"]).is_none()
+}
+
 pub(crate) fn is_extern_spec(tcx: TyCtxt, def_id: DefId) -> bool {
     get_attr(tcx.get_attrs_unchecked(def_id), &["creusot", "extern_spec"]).is_some()
 }
diff --git a/creusot/tests/should_fail/bad_law.stderr b/creusot/tests/should_fail/bad_law.stderr
index f88d1b5abb..0fa9046af0 100644
--- a/creusot/tests/should_fail/bad_law.stderr
+++ b/creusot/tests/should_fail/bad_law.stderr
@@ -4,7 +4,7 @@ error[creusot]: Laws cannot have additional generic parameters
 6 |     fn my_law<T>(x: T);
   |     ^^^^^^^^^^^^^^^^^^^
 
-Ghost != Program
+Logic != Program
 error[creusot]: Expected `my_law` to be a program function as specified by the trait declaration
   --> bad_law.rs:10:5
    |
diff --git a/creusot/tests/should_succeed/bdd.mlcfg b/creusot/tests/should_succeed/bdd.mlcfg
index b2e18b4e7c..61a96dad87 100644
--- a/creusot/tests/should_succeed/bdd.mlcfg
+++ b/creusot/tests/should_succeed/bdd.mlcfg
@@ -3996,7 +3996,7 @@ module CreusotContracts_Logic_Ord_Impl3_CmpLog
   use prelude.Int
   use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
   function cmp_log (self : int) (o : int) : Core_Cmp_Ordering_Type.t_ordering =
-    [#"../../../../creusot-contracts/src/logic/ord.rs" 76 12 85 17] if self < o then
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 137 12 146 17] if self < o then
       Core_Cmp_Ordering_Type.C_Less
     else
       if self = o then Core_Cmp_Ordering_Type.C_Equal else Core_Cmp_Ordering_Type.C_Greater
@@ -4015,6 +4015,180 @@ module Core_Cmp_Impls_Impl63_Cmp_Interface
   val cmp (self : uint64) (other : uint64) : Core_Cmp_Ordering_Type.t_ordering
     ensures { [#"../../../../creusot-contracts/src/std/cmp.rs" 44 26 44 85] result = CmpLog0.cmp_log (DeepModel0.deep_model self) (DeepModel0.deep_model other) }
     
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Stub
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Interface
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : ()
+  val cmp_le_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_le_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 79 12 79 14] ()
+  val cmp_le_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_le_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Stub
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Interface
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : ()
+  val cmp_lt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_lt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 85 12 85 14] ()
+  val cmp_lt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_lt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Stub
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Interface
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : ()
+  val cmp_ge_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_ge_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 91 12 91 14] ()
+  val cmp_ge_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_ge_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Stub
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Interface
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : ()
+  val cmp_gt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_gt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 97 12 97 14] ()
+  val cmp_gt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_gt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl_Stub
+  use prelude.Int
+  function refl (_1 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl_Interface
+  use prelude.Int
+  function refl (_1 : int) : ()
+  val refl (_1 : int) : ()
+    ensures { result = refl _1 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl
+  use prelude.Int
+  function refl (_1 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 103 12 103 14] ()
+  val refl (_1 : int) : ()
+    ensures { result = refl _1 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans_Stub
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans_Interface
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+  val trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+    ensures { result = trans _1 _2 _3 _4 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 109 12 109 14] ()
+  val trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+    ensures { result = trans _1 _2 _3 _4 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1_Stub
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1_Interface
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : ()
+  val antisym1 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym1 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 115 12 115 14] ()
+  val antisym1 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym1 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2_Stub
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2_Interface
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : ()
+  val antisym2 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym2 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 121 12 121 14] ()
+  val antisym2 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym2 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp_Stub
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp_Interface
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : ()
+  val eq_cmp (_1 : int) (_2 : int) : ()
+    ensures { result = eq_cmp _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 127 12 127 14] ()
+  val eq_cmp (_1 : int) (_2 : int) : ()
+    ensures { result = eq_cmp _1 _2 }
+    
 end
 module Bdd_Impl11_And_Interface
   use prelude.Borrow
@@ -4102,6 +4276,16 @@ module Bdd_Impl11_And
     type t = (Bdd_Bdd_Type.t_bdd, Bdd_Bdd_Type.t_bdd),
     predicate Inv0.inv = Inv4.inv,
     axiom .
+  clone CreusotContracts_Logic_Ord_Impl3_EqCmp_Interface as EqCmp0
+  clone CreusotContracts_Logic_Ord_Impl3_Antisym2_Interface as Antisym20
+  clone CreusotContracts_Logic_Ord_Impl3_Antisym1_Interface as Antisym10
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  clone CreusotContracts_Logic_Ord_Impl3_Trans_Interface as Trans0
+  clone CreusotContracts_Logic_Ord_Impl3_Refl_Interface as Refl0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Interface as CmpGtLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Interface as CmpGeLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Interface as CmpLtLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Interface as CmpLeLog0
   clone Bdd_Hashmap_Impl0_ShallowModel_Interface as ShallowModel1 with
     type k = (Bdd_Bdd_Type.t_bdd, Bdd_Bdd_Type.t_bdd),
     type v = Bdd_Bdd_Type.t_bdd,
@@ -4140,7 +4324,6 @@ module Bdd_Impl11_And
     type DeepModelTy1.deepModelTy = uint64,
     function DeepModel0.deep_model = DeepModel3.deep_model,
     function DeepModel1.deep_model = DeepModel3.deep_model
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
   clone CreusotContracts_Logic_Ord_Impl3_CmpLog as CmpLog0
   clone CreusotContracts_Std1_Num_Impl10_DeepModel as DeepModel1
   clone CreusotContracts_Invariant_Inv_Interface as Inv1 with
diff --git a/creusot/tests/should_succeed/bdd/why3session.xml b/creusot/tests/should_succeed/bdd/why3session.xml
index 7f74e91a5a..73f9d98207 100644
--- a/creusot/tests/should_succeed/bdd/why3session.xml
+++ b/creusot/tests/should_succeed/bdd/why3session.xml
@@ -4,6 +4,8 @@
 <why3session shape_version="6">
 <prover id="0" name="CVC4" version="1.8" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="2.5.1" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="2" name="Z3" version="4.11.2" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="3" name="Alt-Ergo" version="2.4.2" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Z3" version="4.12.2" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="6" name="CVC5" version="1.0.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <file format="mlcfg" proved="true">
@@ -448,94 +450,94 @@
  <goal name="and&#39;vc" expl="VC for and" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="and&#39;vc.0" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.014341" steps="26"/></proof>
+  <proof prover="3"><result status="valid" time="0.014341" steps="26"/></proof>
   </goal>
   <goal name="and&#39;vc.1" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.017227" steps="34"/></proof>
+  <proof prover="3"><result status="valid" time="0.017227" steps="34"/></proof>
   </goal>
   <goal name="and&#39;vc.2" expl="variant decrease" proved="true">
-  <proof prover="1"><result status="valid" time="0.104687" steps="629"/></proof>
+  <proof prover="3"><result status="valid" time="0.104687" steps="628"/></proof>
   </goal>
   <goal name="and&#39;vc.3" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.165808" steps="997"/></proof>
+  <proof prover="3"><result status="valid" time="0.165808" steps="999"/></proof>
   </goal>
   <goal name="and&#39;vc.4" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.023521" steps="70"/></proof>
+  <proof prover="3"><result status="valid" time="0.023521" steps="70"/></proof>
   </goal>
   <goal name="and&#39;vc.5" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.023489" steps="87"/></proof>
+  <proof prover="3"><result status="valid" time="0.023489" steps="86"/></proof>
   </goal>
   <goal name="and&#39;vc.6" expl="variant decrease" proved="true">
-  <proof prover="1"><result status="valid" time="0.175962" steps="941"/></proof>
+  <proof prover="3"><result status="valid" time="0.046935" steps="940"/></proof>
   </goal>
   <goal name="and&#39;vc.7" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.406226" steps="1849"/></proof>
+  <proof prover="3"><result status="valid" time="0.112583" steps="1851"/></proof>
   </goal>
   <goal name="and&#39;vc.8" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.055781" steps="311"/></proof>
+  <proof prover="3"><result status="valid" time="0.055781" steps="311"/></proof>
   </goal>
   <goal name="and&#39;vc.9" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.043391" steps="102"/></proof>
+  <proof prover="3"><result status="valid" time="0.043391" steps="100"/></proof>
   </goal>
   <goal name="and&#39;vc.10" expl="variant decrease" proved="true">
-  <proof prover="1"><result status="valid" time="0.116983" steps="735"/></proof>
+  <proof prover="3"><result status="valid" time="0.116983" steps="733"/></proof>
   </goal>
   <goal name="and&#39;vc.11" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.264085" steps="1084"/></proof>
+  <proof prover="3"><result status="valid" time="0.054904" steps="1085"/></proof>
   </goal>
   <goal name="and&#39;vc.12" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.314295" steps="1390"/></proof>
+  <proof prover="3"><result status="valid" time="0.072346" steps="1393"/></proof>
   </goal>
   <goal name="and&#39;vc.13" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.060713" steps="88"/></proof>
+  <proof prover="3"><result status="valid" time="0.060713" steps="88"/></proof>
   </goal>
   <goal name="and&#39;vc.14" expl="variant decrease" proved="true">
-  <proof prover="1"><result status="valid" time="0.210758" steps="1057"/></proof>
+  <proof prover="3"><result status="valid" time="0.052060" steps="1055"/></proof>
   </goal>
   <goal name="and&#39;vc.15" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.375963" steps="2024"/></proof>
+  <proof prover="3"><result status="valid" time="0.123282" steps="2030"/></proof>
   </goal>
   <goal name="and&#39;vc.16" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.452204" steps="2488"/></proof>
+  <proof prover="3"><result status="valid" time="0.153971" steps="2495"/></proof>
   </goal>
   <goal name="and&#39;vc.17" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.047254" steps="102"/></proof>
+  <proof prover="3"><result status="valid" time="0.047254" steps="100"/></proof>
   </goal>
   <goal name="and&#39;vc.18" expl="variant decrease" proved="true">
-  <proof prover="1"><result status="valid" time="0.109249" steps="628"/></proof>
+  <proof prover="3"><result status="valid" time="0.109249" steps="627"/></proof>
   </goal>
   <goal name="and&#39;vc.19" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.035982" steps="68"/></proof>
+  <proof prover="3"><result status="valid" time="0.035982" steps="68"/></proof>
   </goal>
   <goal name="and&#39;vc.20" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.170482" steps="997"/></proof>
+  <proof prover="3"><result status="valid" time="0.050016" steps="998"/></proof>
   </goal>
   <goal name="and&#39;vc.21" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.030529" steps="87"/></proof>
+  <proof prover="3"><result status="valid" time="0.030529" steps="87"/></proof>
   </goal>
   <goal name="and&#39;vc.22" expl="variant decrease" proved="true">
-  <proof prover="1"><result status="valid" time="0.127493" steps="938"/></proof>
+  <proof prover="3"><result status="valid" time="0.127493" steps="938"/></proof>
   </goal>
   <goal name="and&#39;vc.23" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.076955" steps="274"/></proof>
+  <proof prover="3"><result status="valid" time="0.076955" steps="274"/></proof>
   </goal>
   <goal name="and&#39;vc.24" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.311052" steps="1941"/></proof>
+  <proof prover="3"><result status="valid" time="0.116922" steps="1942"/></proof>
   </goal>
   <goal name="and&#39;vc.25" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.036395" steps="102"/></proof>
+  <proof prover="3"><result status="valid" time="0.036395" steps="100"/></proof>
   </goal>
   <goal name="and&#39;vc.26" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.016491" steps="40"/></proof>
+  <proof prover="3"><result status="valid" time="0.016491" steps="40"/></proof>
   </goal>
   <goal name="and&#39;vc.27" expl="type invariant" proved="true">
-  <proof prover="1"><result status="valid" time="0.016388" steps="40"/></proof>
+  <proof prover="3"><result status="valid" time="0.016388" steps="40"/></proof>
   </goal>
   <goal name="and&#39;vc.28" expl="unreachable point" proved="true">
   <proof prover="6"><result status="valid" time="0.085307" steps="5854"/></proof>
   </goal>
   <goal name="and&#39;vc.29" expl="precondition" proved="true">
-  <proof prover="4"><result status="valid" time="0.251503" steps="251609"/></proof>
+  <proof prover="2"><result status="valid" time="0.067880" steps="258665"/></proof>
   </goal>
   <goal name="and&#39;vc.30" expl="precondition" proved="true">
   <proof prover="6"><result status="valid" time="0.091440" steps="8389"/></proof>
@@ -549,13 +551,13 @@
      <goal name="and&#39;vc.31.0.0.0" expl="precondition" proved="true">
      <transf name="split_vc" proved="true" >
       <goal name="and&#39;vc.31.0.0.0.0" expl="precondition" proved="true">
-      <proof prover="4"><result status="valid" time="0.523616" steps="544049"/></proof>
+      <proof prover="2"><result status="valid" time="0.084472" steps="395875"/></proof>
       </goal>
       <goal name="and&#39;vc.31.0.0.0.1" expl="precondition" proved="true">
-      <proof prover="4"><result status="valid" time="0.209960" steps="216783"/></proof>
+      <proof prover="2"><result status="valid" time="0.209960" steps="532284"/></proof>
       </goal>
       <goal name="and&#39;vc.31.0.0.0.2" expl="precondition" proved="true">
-      <proof prover="4"><result status="valid" time="0.485236" steps="451427"/></proof>
+      <proof prover="2"><result status="valid" time="0.104813" steps="458944"/></proof>
       </goal>
      </transf>
      </goal>
@@ -570,13 +572,13 @@
      <goal name="and&#39;vc.31.1.0.0" expl="precondition" proved="true">
      <transf name="split_vc" proved="true" >
       <goal name="and&#39;vc.31.1.0.0.0" expl="precondition" proved="true">
-      <proof prover="6"><result status="valid" time="0.721219" steps="42233"/></proof>
+      <proof prover="6"><result status="valid" time="0.252434" steps="42233"/></proof>
       </goal>
       <goal name="and&#39;vc.31.1.0.0.1" expl="precondition" proved="true">
-      <proof prover="4"><result status="valid" time="0.260183" steps="280230"/></proof>
+      <proof prover="2"><result status="valid" time="0.086875" steps="396721"/></proof>
       </goal>
       <goal name="and&#39;vc.31.1.0.0.2" expl="precondition" proved="true">
-      <proof prover="4"><result status="valid" time="0.475145" steps="462414"/></proof>
+      <proof prover="2"><result status="valid" time="0.120648" steps="541351"/></proof>
       </goal>
      </transf>
      </goal>
@@ -587,16 +589,16 @@
   </transf>
   </goal>
   <goal name="and&#39;vc.32" expl="precondition" proved="true">
-  <proof prover="4"><result status="valid" time="0.116839" steps="140173"/></proof>
+  <proof prover="2"><result status="valid" time="0.116839" steps="146074"/></proof>
   </goal>
   <goal name="and&#39;vc.33" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.029470" steps="44"/></proof>
+  <proof prover="3"><result status="valid" time="0.029470" steps="43"/></proof>
   </goal>
   <goal name="and&#39;vc.34" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.126516" steps="45"/></proof>
+  <proof prover="3"><result status="valid" time="0.126516" steps="43"/></proof>
   </goal>
   <goal name="and&#39;vc.35" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.137980" steps="46"/></proof>
+  <proof prover="3"><result status="valid" time="0.137980" steps="45"/></proof>
   </goal>
   <goal name="and&#39;vc.36" expl="type invariant" proved="true">
   <transf name="split_vc" proved="true" >
@@ -605,12 +607,12 @@
     <goal name="and&#39;vc.36.0.0" expl="type invariant" proved="true">
     <transf name="split_vc" proved="true" >
      <goal name="and&#39;vc.36.0.0.0" expl="type invariant" proved="true">
-     <proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="1.720867" steps="71014"/></proof>
+     <proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="0.942893" steps="99615"/></proof>
      </goal>
      <goal name="and&#39;vc.36.0.0.1" expl="type invariant" proved="true">
      <transf name="split_vc" proved="true" >
       <goal name="and&#39;vc.36.0.0.1.0" expl="type invariant" proved="true">
-      <proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="1.926729" steps="81700"/></proof>
+      <proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="0.770930" steps="83465"/></proof>
       </goal>
      </transf>
      </goal>
@@ -625,13 +627,13 @@
      <goal name="and&#39;vc.36.1.0.0" expl="type invariant" proved="true">
      <transf name="split_vc" proved="true" >
       <goal name="and&#39;vc.36.1.0.0.0" expl="type invariant" proved="true">
-      <proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="6.364003" steps="193664"/></proof>
+      <proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="2.235378" steps="208186"/></proof>
       </goal>
       <goal name="and&#39;vc.36.1.0.0.1" expl="type invariant" proved="true">
-      <proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="7.413384" steps="219024"/></proof>
+      <proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="2.518085" steps="220252"/></proof>
       </goal>
       <goal name="and&#39;vc.36.1.0.0.2" expl="type invariant" proved="true">
-      <proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="6.640251" steps="204514"/></proof>
+      <proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="2.246086" steps="206124"/></proof>
       </goal>
      </transf>
      </goal>
@@ -646,14 +648,14 @@
      <goal name="and&#39;vc.36.2.0.0" expl="type invariant" proved="true">
      <transf name="split_vc" proved="true" >
       <goal name="and&#39;vc.36.2.0.0.0" expl="type invariant" proved="true">
-      <proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="3.132695" steps="114010"/></proof>
+      <proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="1.076810" steps="114779"/></proof>
       </goal>
      </transf>
      </goal>
      <goal name="and&#39;vc.36.2.0.1" expl="type invariant" proved="true">
      <transf name="split_vc" proved="true" >
       <goal name="and&#39;vc.36.2.0.1.0" expl="type invariant" proved="true">
-      <proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="4.401255" steps="148781"/></proof>
+      <proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="1.640519" steps="161122"/></proof>
       </goal>
      </transf>
      </goal>
@@ -664,28 +666,28 @@
   </transf>
   </goal>
   <goal name="and&#39;vc.37" expl="postcondition" proved="true">
-  <proof prover="4"><result status="valid" time="0.532894" steps="533439"/></proof>
+  <proof prover="2"><result status="valid" time="0.148957" steps="549303"/></proof>
   </goal>
   <goal name="and&#39;vc.38" expl="postcondition" proved="true">
-  <proof prover="4"><result status="valid" time="0.211103" steps="268860"/></proof>
+  <proof prover="2"><result status="valid" time="0.211103" steps="1215556"/></proof>
   </goal>
   <goal name="and&#39;vc.39" expl="postcondition" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="and&#39;vc.39.0" expl="postcondition" proved="true">
    <transf name="split_vc" proved="true" >
     <goal name="and&#39;vc.39.0.0" expl="postcondition" proved="true">
-    <proof prover="6"><result status="valid" time="0.271173" steps="20149"/></proof>
+    <proof prover="6"><result status="valid" time="0.119644" steps="20149"/></proof>
     </goal>
     <goal name="and&#39;vc.39.0.1" expl="postcondition" proved="true">
     <transf name="split_vc" proved="true" >
      <goal name="and&#39;vc.39.0.1.0" expl="postcondition" proved="true">
-     <proof prover="4"><result status="valid" time="0.187911" steps="188866"/></proof>
+     <proof prover="2"><result status="valid" time="0.041714" steps="199045"/></proof>
      </goal>
      <goal name="and&#39;vc.39.0.1.1" expl="postcondition" proved="true">
-     <proof prover="4"><result status="valid" time="0.348120" steps="511952"/></proof>
+     <proof prover="2"><result status="valid" time="0.192811" steps="822121"/></proof>
      </goal>
      <goal name="and&#39;vc.39.0.1.2" expl="postcondition" proved="true">
-     <proof prover="1"><result status="valid" time="0.057312" steps="80"/></proof>
+     <proof prover="3"><result status="valid" time="0.057312" steps="80"/></proof>
      </goal>
     </transf>
     </goal>
@@ -694,7 +696,7 @@
    <goal name="and&#39;vc.39.1" expl="postcondition" proved="true">
    <transf name="split_vc" proved="true" >
     <goal name="and&#39;vc.39.1.0" expl="postcondition" proved="true">
-    <proof prover="4"><result status="valid" time="0.273346" steps="265170"/></proof>
+    <proof prover="2"><result status="valid" time="0.034327" steps="178213"/></proof>
     </goal>
     <goal name="and&#39;vc.39.1.1" expl="postcondition" proved="true">
     <transf name="split_vc" proved="true" >
@@ -702,10 +704,10 @@
      <proof prover="6"><result status="valid" time="0.088131" steps="12579"/></proof>
      </goal>
      <goal name="and&#39;vc.39.1.1.1" expl="postcondition" proved="true">
-     <proof prover="4"><result status="valid" time="0.206378" steps="398138"/></proof>
+     <proof prover="2"><result status="valid" time="0.206378" steps="406000"/></proof>
      </goal>
      <goal name="and&#39;vc.39.1.1.2" expl="postcondition" proved="true">
-     <proof prover="1"><result status="valid" time="0.052401" steps="80"/></proof>
+     <proof prover="3"><result status="valid" time="0.052401" steps="80"/></proof>
      </goal>
     </transf>
     </goal>
@@ -714,7 +716,7 @@
    <goal name="and&#39;vc.39.2" expl="postcondition" proved="true">
    <transf name="split_vc" proved="true" >
     <goal name="and&#39;vc.39.2.0" expl="postcondition" proved="true">
-    <proof prover="4"><result status="valid" time="0.267631" steps="273966"/></proof>
+    <proof prover="2"><result status="valid" time="0.058120" steps="263688"/></proof>
     </goal>
     <goal name="and&#39;vc.39.2.1" expl="postcondition" proved="true">
     <transf name="split_vc" proved="true" >
@@ -724,12 +726,12 @@
      <goal name="and&#39;vc.39.2.1.1" expl="postcondition" proved="true">
      <transf name="split_vc" proved="true" >
       <goal name="and&#39;vc.39.2.1.1.0" expl="postcondition" proved="true">
-      <proof prover="6"><result status="valid" time="0.921127" steps="60224"/></proof>
+      <proof prover="6"><result status="valid" time="0.330500" steps="60232"/></proof>
       </goal>
      </transf>
      </goal>
      <goal name="and&#39;vc.39.2.1.2" expl="postcondition" proved="true">
-     <proof prover="6"><result status="valid" time="0.199316" steps="14208"/></proof>
+     <proof prover="6"><result status="valid" time="0.068475" steps="14208"/></proof>
      </goal>
     </transf>
     </goal>
@@ -740,10 +742,10 @@
   <goal name="and&#39;vc.40" expl="postcondition" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="and&#39;vc.40.0" expl="postcondition" proved="true">
-   <proof prover="4"><result status="valid" time="0.442270" steps="424427"/></proof>
+   <proof prover="2"><result status="valid" time="0.050306" steps="231721"/></proof>
    </goal>
    <goal name="and&#39;vc.40.1" expl="postcondition" proved="true">
-   <proof prover="6"><result status="valid" time="0.318785" steps="30502"/></proof>
+   <proof prover="6"><result status="valid" time="0.119851" steps="30502"/></proof>
    </goal>
   </transf>
   </goal>
diff --git a/creusot/tests/should_succeed/bdd/why3shapes.gz b/creusot/tests/should_succeed/bdd/why3shapes.gz
index 2c7cabf112..d00db57426 100644
Binary files a/creusot/tests/should_succeed/bdd/why3shapes.gz and b/creusot/tests/should_succeed/bdd/why3shapes.gz differ
diff --git a/creusot/tests/should_succeed/bug/387.mlcfg b/creusot/tests/should_succeed/bug/387.mlcfg
index 7d5b0ddbc1..03541c9e39 100644
--- a/creusot/tests/should_succeed/bug/387.mlcfg
+++ b/creusot/tests/should_succeed/bug/387.mlcfg
@@ -310,6 +310,180 @@ module CreusotContracts_Logic_Ord_Impl3_LtLog
   val lt_log (self : int) (_2 : int) : bool
     ensures { result = lt_log self _2 }
     
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Stub
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Interface
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : ()
+  val cmp_le_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_le_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 79 12 79 14] ()
+  val cmp_le_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_le_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Stub
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Interface
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : ()
+  val cmp_lt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_lt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 85 12 85 14] ()
+  val cmp_lt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_lt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Stub
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Interface
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : ()
+  val cmp_ge_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_ge_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 91 12 91 14] ()
+  val cmp_ge_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_ge_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Stub
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Interface
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : ()
+  val cmp_gt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_gt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 97 12 97 14] ()
+  val cmp_gt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_gt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl_Stub
+  use prelude.Int
+  function refl (_1 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl_Interface
+  use prelude.Int
+  function refl (_1 : int) : ()
+  val refl (_1 : int) : ()
+    ensures { result = refl _1 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl
+  use prelude.Int
+  function refl (_1 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 103 12 103 14] ()
+  val refl (_1 : int) : ()
+    ensures { result = refl _1 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans_Stub
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans_Interface
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+  val trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+    ensures { result = trans _1 _2 _3 _4 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 109 12 109 14] ()
+  val trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+    ensures { result = trans _1 _2 _3 _4 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1_Stub
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1_Interface
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : ()
+  val antisym1 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym1 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 115 12 115 14] ()
+  val antisym1 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym1 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2_Stub
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2_Interface
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : ()
+  val antisym2 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym2 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 121 12 121 14] ()
+  val antisym2 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym2 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp_Stub
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp_Interface
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : ()
+  val eq_cmp (_1 : int) (_2 : int) : ()
+    ensures { result = eq_cmp _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 127 12 127 14] ()
+  val eq_cmp (_1 : int) (_2 : int) : ()
+    ensures { result = eq_cmp _1 _2 }
+    
 end
 module C387_Impl0_Height_Interface
   use prelude.Borrow
@@ -322,6 +496,16 @@ module C387_Impl0_Height
   use prelude.Int
   use prelude.UInt64
   use prelude.Borrow
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  clone CreusotContracts_Logic_Ord_Impl3_EqCmp_Interface as EqCmp0
+  clone CreusotContracts_Logic_Ord_Impl3_Antisym2_Interface as Antisym20
+  clone CreusotContracts_Logic_Ord_Impl3_Antisym1_Interface as Antisym10
+  clone CreusotContracts_Logic_Ord_Impl3_Trans_Interface as Trans0
+  clone CreusotContracts_Logic_Ord_Impl3_Refl_Interface as Refl0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Interface as CmpGtLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Interface as CmpGeLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Interface as CmpLtLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Interface as CmpLeLog0
   clone CreusotContracts_Invariant_Inv_Interface as Inv0 with
     type t = uint64
   clone TyInv_Trivial as TyInv_Trivial0 with
diff --git a/creusot/tests/should_succeed/constrained_types.mlcfg b/creusot/tests/should_succeed/constrained_types.mlcfg
index b5f315e7ae..d4e89a7551 100644
--- a/creusot/tests/should_succeed/constrained_types.mlcfg
+++ b/creusot/tests/should_succeed/constrained_types.mlcfg
@@ -192,7 +192,7 @@ module CreusotContracts_Logic_Ord_Impl1_LtLog
   clone CreusotContracts_Logic_Ord_OrdLogic_LtLog_Stub as LtLog0 with
     type self = b
   function lt_log (self : (a, b)) (o : (a, b)) : bool =
-    [#"../../../../creusot-contracts/src/logic/ord.rs" 269 20 269 67] (let (a, _) = self in a) = (let (a, _) = o in a) /\ LtLog0.lt_log (let (_, a) = self in a) (let (_, a) = o in a) \/ LtLog1.lt_log (let (a, _) = self in a) (let (a, _) = o in a)
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 240 20 240 67] (let (a, _) = self in a) = (let (a, _) = o in a) /\ LtLog0.lt_log (let (_, a) = self in a) (let (_, a) = o in a) \/ LtLog1.lt_log (let (a, _) = self in a) (let (a, _) = o in a)
   val lt_log (self : (a, b)) (o : (a, b)) : bool
     ensures { result = lt_log self o }
     
@@ -283,6 +283,207 @@ module CreusotContracts_Std1_Tuples_Impl4_DeepModel
   val deep_model (self : (a, b)) : (DeepModelTy0.deepModelTy, DeepModelTy1.deepModelTy)
     ensures { result = deep_model self }
     
+end
+module CreusotContracts_Logic_Ord_Impl1_CmpLeLog_Stub
+  type a
+  type b
+  function cmp_le_log (_1 : (a, b)) (_2 : (a, b)) : ()
+end
+module CreusotContracts_Logic_Ord_Impl1_CmpLeLog_Interface
+  type a
+  type b
+  function cmp_le_log (_1 : (a, b)) (_2 : (a, b)) : ()
+  val cmp_le_log (_1 : (a, b)) (_2 : (a, b)) : ()
+    ensures { result = cmp_le_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl1_CmpLeLog
+  type a
+  type b
+  function cmp_le_log (_1 : (a, b)) (_2 : (a, b)) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 79 12 79 14] ()
+  val cmp_le_log (_1 : (a, b)) (_2 : (a, b)) : ()
+    ensures { result = cmp_le_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl1_CmpLtLog_Stub
+  type a
+  type b
+  function cmp_lt_log (_1 : (a, b)) (_2 : (a, b)) : ()
+end
+module CreusotContracts_Logic_Ord_Impl1_CmpLtLog_Interface
+  type a
+  type b
+  function cmp_lt_log (_1 : (a, b)) (_2 : (a, b)) : ()
+  val cmp_lt_log (_1 : (a, b)) (_2 : (a, b)) : ()
+    ensures { result = cmp_lt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl1_CmpLtLog
+  type a
+  type b
+  function cmp_lt_log (_1 : (a, b)) (_2 : (a, b)) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 85 12 85 14] ()
+  val cmp_lt_log (_1 : (a, b)) (_2 : (a, b)) : ()
+    ensures { result = cmp_lt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl1_CmpGeLog_Stub
+  type a
+  type b
+  function cmp_ge_log (_1 : (a, b)) (_2 : (a, b)) : ()
+end
+module CreusotContracts_Logic_Ord_Impl1_CmpGeLog_Interface
+  type a
+  type b
+  function cmp_ge_log (_1 : (a, b)) (_2 : (a, b)) : ()
+  val cmp_ge_log (_1 : (a, b)) (_2 : (a, b)) : ()
+    ensures { result = cmp_ge_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl1_CmpGeLog
+  type a
+  type b
+  function cmp_ge_log (_1 : (a, b)) (_2 : (a, b)) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 91 12 91 14] ()
+  val cmp_ge_log (_1 : (a, b)) (_2 : (a, b)) : ()
+    ensures { result = cmp_ge_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl1_CmpGtLog_Stub
+  type a
+  type b
+  function cmp_gt_log (_1 : (a, b)) (_2 : (a, b)) : ()
+end
+module CreusotContracts_Logic_Ord_Impl1_CmpGtLog_Interface
+  type a
+  type b
+  function cmp_gt_log (_1 : (a, b)) (_2 : (a, b)) : ()
+  val cmp_gt_log (_1 : (a, b)) (_2 : (a, b)) : ()
+    ensures { result = cmp_gt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl1_CmpGtLog
+  type a
+  type b
+  function cmp_gt_log (_1 : (a, b)) (_2 : (a, b)) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 97 12 97 14] ()
+  val cmp_gt_log (_1 : (a, b)) (_2 : (a, b)) : ()
+    ensures { result = cmp_gt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl1_Refl_Stub
+  type a
+  type b
+  function refl (_1 : (a, b)) : ()
+end
+module CreusotContracts_Logic_Ord_Impl1_Refl_Interface
+  type a
+  type b
+  function refl (_1 : (a, b)) : ()
+  val refl (_1 : (a, b)) : ()
+    ensures { result = refl _1 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl1_Refl
+  type a
+  type b
+  function refl (_1 : (a, b)) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 103 12 103 14] ()
+  val refl (_1 : (a, b)) : ()
+    ensures { result = refl _1 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl1_Trans_Stub
+  type a
+  type b
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : (a, b)) (_2 : (a, b)) (_3 : (a, b)) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+end
+module CreusotContracts_Logic_Ord_Impl1_Trans_Interface
+  type a
+  type b
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : (a, b)) (_2 : (a, b)) (_3 : (a, b)) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+  val trans (_1 : (a, b)) (_2 : (a, b)) (_3 : (a, b)) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+    ensures { result = trans _1 _2 _3 _4 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl1_Trans
+  type a
+  type b
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : (a, b)) (_2 : (a, b)) (_3 : (a, b)) (_4 : Core_Cmp_Ordering_Type.t_ordering) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 109 12 109 14] ()
+  val trans (_1 : (a, b)) (_2 : (a, b)) (_3 : (a, b)) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+    ensures { result = trans _1 _2 _3 _4 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl1_Antisym1_Stub
+  type a
+  type b
+  function antisym1 (_1 : (a, b)) (_2 : (a, b)) : ()
+end
+module CreusotContracts_Logic_Ord_Impl1_Antisym1_Interface
+  type a
+  type b
+  function antisym1 (_1 : (a, b)) (_2 : (a, b)) : ()
+  val antisym1 (_1 : (a, b)) (_2 : (a, b)) : ()
+    ensures { result = antisym1 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl1_Antisym1
+  type a
+  type b
+  function antisym1 (_1 : (a, b)) (_2 : (a, b)) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 115 12 115 14] ()
+  val antisym1 (_1 : (a, b)) (_2 : (a, b)) : ()
+    ensures { result = antisym1 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl1_Antisym2_Stub
+  type a
+  type b
+  function antisym2 (_1 : (a, b)) (_2 : (a, b)) : ()
+end
+module CreusotContracts_Logic_Ord_Impl1_Antisym2_Interface
+  type a
+  type b
+  function antisym2 (_1 : (a, b)) (_2 : (a, b)) : ()
+  val antisym2 (_1 : (a, b)) (_2 : (a, b)) : ()
+    ensures { result = antisym2 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl1_Antisym2
+  type a
+  type b
+  function antisym2 (_1 : (a, b)) (_2 : (a, b)) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 121 12 121 14] ()
+  val antisym2 (_1 : (a, b)) (_2 : (a, b)) : ()
+    ensures { result = antisym2 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl1_EqCmp_Stub
+  type a
+  type b
+  function eq_cmp (_1 : (a, b)) (_2 : (a, b)) : ()
+end
+module CreusotContracts_Logic_Ord_Impl1_EqCmp_Interface
+  type a
+  type b
+  function eq_cmp (_1 : (a, b)) (_2 : (a, b)) : ()
+  val eq_cmp (_1 : (a, b)) (_2 : (a, b)) : ()
+    ensures { result = eq_cmp _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl1_EqCmp
+  type a
+  type b
+  function eq_cmp (_1 : (a, b)) (_2 : (a, b)) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 127 12 127 14] ()
+  val eq_cmp (_1 : (a, b)) (_2 : (a, b)) : ()
+    ensures { result = eq_cmp _1 _2 }
+    
 end
 module CreusotContracts_Logic_Ord_Impl3_LtLog_Stub
   use prelude.Int
@@ -325,6 +526,180 @@ module CreusotContracts_Std1_Num_Impl7_DeepModel
   val deep_model (self : uint32) : int
     ensures { result = deep_model self }
     
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Stub
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Interface
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : ()
+  val cmp_le_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_le_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 79 12 79 14] ()
+  val cmp_le_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_le_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Stub
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Interface
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : ()
+  val cmp_lt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_lt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 85 12 85 14] ()
+  val cmp_lt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_lt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Stub
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Interface
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : ()
+  val cmp_ge_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_ge_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 91 12 91 14] ()
+  val cmp_ge_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_ge_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Stub
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Interface
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : ()
+  val cmp_gt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_gt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 97 12 97 14] ()
+  val cmp_gt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_gt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl_Stub
+  use prelude.Int
+  function refl (_1 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl_Interface
+  use prelude.Int
+  function refl (_1 : int) : ()
+  val refl (_1 : int) : ()
+    ensures { result = refl _1 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl
+  use prelude.Int
+  function refl (_1 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 103 12 103 14] ()
+  val refl (_1 : int) : ()
+    ensures { result = refl _1 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans_Stub
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans_Interface
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+  val trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+    ensures { result = trans _1 _2 _3 _4 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 109 12 109 14] ()
+  val trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+    ensures { result = trans _1 _2 _3 _4 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1_Stub
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1_Interface
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : ()
+  val antisym1 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym1 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 115 12 115 14] ()
+  val antisym1 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym1 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2_Stub
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2_Interface
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : ()
+  val antisym2 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym2 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 121 12 121 14] ()
+  val antisym2 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym2 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp_Stub
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp_Interface
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : ()
+  val eq_cmp (_1 : int) (_2 : int) : ()
+    ensures { result = eq_cmp _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 127 12 127 14] ()
+  val eq_cmp (_1 : int) (_2 : int) : ()
+    ensures { result = eq_cmp _1 _2 }
+    
 end
 module ConstrainedTypes_UsesConcreteInstance_Interface
   use prelude.Int
@@ -336,9 +711,46 @@ module ConstrainedTypes_UsesConcreteInstance
   use prelude.Int
   use prelude.UInt32
   use prelude.Borrow
+  clone CreusotContracts_Logic_Ord_Impl3_EqCmp_Interface as EqCmp1
+  clone CreusotContracts_Logic_Ord_Impl3_Antisym2_Interface as Antisym21
+  clone CreusotContracts_Logic_Ord_Impl3_Antisym1_Interface as Antisym11
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  clone CreusotContracts_Logic_Ord_Impl3_Trans_Interface as Trans1
+  clone CreusotContracts_Logic_Ord_Impl3_Refl_Interface as Refl1
+  clone CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Interface as CmpGtLog1
+  clone CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Interface as CmpGeLog1
+  clone CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Interface as CmpLtLog1
+  clone CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Interface as CmpLeLog1
   clone CreusotContracts_Std1_Num_Impl7_DeepModel as DeepModel2
   clone CreusotContracts_Logic_Ord_Impl3_LtLog as LtLog1
   use prelude.Int
+  clone CreusotContracts_Logic_Ord_Impl1_EqCmp_Interface as EqCmp0 with
+    type a = int,
+    type b = int
+  clone CreusotContracts_Logic_Ord_Impl1_Antisym2_Interface as Antisym20 with
+    type a = int,
+    type b = int
+  clone CreusotContracts_Logic_Ord_Impl1_Antisym1_Interface as Antisym10 with
+    type a = int,
+    type b = int
+  clone CreusotContracts_Logic_Ord_Impl1_Trans_Interface as Trans0 with
+    type a = int,
+    type b = int
+  clone CreusotContracts_Logic_Ord_Impl1_Refl_Interface as Refl0 with
+    type a = int,
+    type b = int
+  clone CreusotContracts_Logic_Ord_Impl1_CmpGtLog_Interface as CmpGtLog0 with
+    type a = int,
+    type b = int
+  clone CreusotContracts_Logic_Ord_Impl1_CmpGeLog_Interface as CmpGeLog0 with
+    type a = int,
+    type b = int
+  clone CreusotContracts_Logic_Ord_Impl1_CmpLtLog_Interface as CmpLtLog0 with
+    type a = int,
+    type b = int
+  clone CreusotContracts_Logic_Ord_Impl1_CmpLeLog_Interface as CmpLeLog0 with
+    type a = int,
+    type b = int
   clone CreusotContracts_Std1_Tuples_Impl4_DeepModel as DeepModel1 with
     type a = uint32,
     type b = uint32,
diff --git a/creusot/tests/should_succeed/constrained_types/why3shapes.gz b/creusot/tests/should_succeed/constrained_types/why3shapes.gz
index bf95b3e0a9..c6053a7397 100644
Binary files a/creusot/tests/should_succeed/constrained_types/why3shapes.gz and b/creusot/tests/should_succeed/constrained_types/why3shapes.gz differ
diff --git a/creusot/tests/should_succeed/instant.mlcfg b/creusot/tests/should_succeed/instant.mlcfg
index 22012ece8b..c254489ec8 100644
--- a/creusot/tests/should_succeed/instant.mlcfg
+++ b/creusot/tests/should_succeed/instant.mlcfg
@@ -809,6 +809,180 @@ module CreusotContracts_Std1_Time_Impl1_DeepModel
     
   axiom deep_model_spec : forall self : Core_Time_Duration_Type.t_duration . ([#"../../../../creusot-contracts/src/std/time.rs" 26 14 26 44] deep_model self = ShallowModel0.shallow_model self) && ([#"../../../../creusot-contracts/src/std/time.rs" 25 14 25 77] deep_model self >= 0 /\ deep_model self <= SecsToNanos0.secs_to_nanos (UInt64.to_int Max0.mAX') + 999999999)
 end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Stub
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Interface
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : ()
+  val cmp_le_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_le_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 79 12 79 14] ()
+  val cmp_le_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_le_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Stub
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Interface
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : ()
+  val cmp_lt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_lt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 85 12 85 14] ()
+  val cmp_lt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_lt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Stub
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Interface
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : ()
+  val cmp_ge_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_ge_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 91 12 91 14] ()
+  val cmp_ge_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_ge_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Stub
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Interface
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : ()
+  val cmp_gt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_gt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 97 12 97 14] ()
+  val cmp_gt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_gt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl_Stub
+  use prelude.Int
+  function refl (_1 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl_Interface
+  use prelude.Int
+  function refl (_1 : int) : ()
+  val refl (_1 : int) : ()
+    ensures { result = refl _1 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl
+  use prelude.Int
+  function refl (_1 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 103 12 103 14] ()
+  val refl (_1 : int) : ()
+    ensures { result = refl _1 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans_Stub
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans_Interface
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+  val trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+    ensures { result = trans _1 _2 _3 _4 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 109 12 109 14] ()
+  val trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+    ensures { result = trans _1 _2 _3 _4 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1_Stub
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1_Interface
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : ()
+  val antisym1 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym1 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 115 12 115 14] ()
+  val antisym1 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym1 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2_Stub
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2_Interface
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : ()
+  val antisym2 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym2 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 121 12 121 14] ()
+  val antisym2 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym2 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp_Stub
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp_Interface
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : ()
+  val eq_cmp (_1 : int) (_2 : int) : ()
+    ensures { result = eq_cmp _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 127 12 127 14] ()
+  val eq_cmp (_1 : int) (_2 : int) : ()
+    ensures { result = eq_cmp _1 _2 }
+    
+end
 module CreusotContracts_Std1_Time_Impl3_DeepModel_Stub
   use prelude.Int
   use Std_Time_Instant_Type as Std_Time_Instant_Type
@@ -1291,7 +1465,7 @@ module CreusotContracts_Logic_Ord_Impl2_CmpLog
   function cmp_log (self : Core_Option_Option_Type.t_option t) (o : Core_Option_Option_Type.t_option t) : Core_Cmp_Ordering_Type.t_ordering
     
    =
-    [#"../../../../creusot-contracts/src/logic/ord.rs" 321 8 326 9] match ((self, o)) with
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 262 8 267 9] match ((self, o)) with
       | (Core_Option_Option_Type.C_None, Core_Option_Option_Type.C_None) -> Core_Cmp_Ordering_Type.C_Equal
       | (Core_Option_Option_Type.C_None, Core_Option_Option_Type.C_Some _) -> Core_Cmp_Ordering_Type.C_Less
       | (Core_Option_Option_Type.C_Some _, Core_Option_Option_Type.C_None) -> Core_Cmp_Ordering_Type.C_Greater
@@ -1304,443 +1478,207 @@ end
 module CreusotContracts_Logic_Ord_Impl2_CmpLeLog_Stub
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  clone CreusotContracts_Logic_Ord_OrdLogic_LeLog_Stub as LeLog0 with
-    type self = Core_Option_Option_Type.t_option t
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  function cmp_le_log (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
+  function cmp_le_log (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
 end
 module CreusotContracts_Logic_Ord_Impl2_CmpLeLog_Interface
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  clone CreusotContracts_Logic_Ord_OrdLogic_LeLog_Stub as LeLog0 with
-    type self = Core_Option_Option_Type.t_option t
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  function cmp_le_log (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
-  val cmp_le_log (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 332 18 332 19] Inv0.inv x}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 332 27 332 28] Inv0.inv y}
-    ensures { [#"../../../../creusot-contracts/src/logic/ord.rs" 331 14 331 64] LeLog0.le_log x y = (CmpLog0.cmp_log x y <> Core_Cmp_Ordering_Type.C_Greater) }
-    ensures { result = cmp_le_log x y }
+  function cmp_le_log (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
+  val cmp_le_log (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
+    ensures { result = cmp_le_log _1 _2 }
     
-  axiom cmp_le_log_spec : forall x : Core_Option_Option_Type.t_option t, y : Core_Option_Option_Type.t_option t . ([#"../../../../creusot-contracts/src/logic/ord.rs" 332 18 332 19] Inv0.inv x) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 332 27 332 28] Inv0.inv y) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 331 14 331 64] LeLog0.le_log x y = (CmpLog0.cmp_log x y <> Core_Cmp_Ordering_Type.C_Greater))
 end
 module CreusotContracts_Logic_Ord_Impl2_CmpLeLog
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  clone CreusotContracts_Logic_Ord_OrdLogic_LeLog_Stub as LeLog0 with
-    type self = Core_Option_Option_Type.t_option t
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  function cmp_le_log (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : () =
-    [#"../../../../creusot-contracts/src/logic/ord.rs" 329 4 329 10] ()
-  val cmp_le_log (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 332 18 332 19] Inv0.inv x}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 332 27 332 28] Inv0.inv y}
-    ensures { [#"../../../../creusot-contracts/src/logic/ord.rs" 331 14 331 64] LeLog0.le_log x y = (CmpLog0.cmp_log x y <> Core_Cmp_Ordering_Type.C_Greater) }
-    ensures { result = cmp_le_log x y }
+  function cmp_le_log (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 79 12 79 14] ()
+  val cmp_le_log (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
+    ensures { result = cmp_le_log _1 _2 }
     
-  axiom cmp_le_log_spec : forall x : Core_Option_Option_Type.t_option t, y : Core_Option_Option_Type.t_option t . ([#"../../../../creusot-contracts/src/logic/ord.rs" 332 18 332 19] Inv0.inv x) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 332 27 332 28] Inv0.inv y) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 331 14 331 64] LeLog0.le_log x y = (CmpLog0.cmp_log x y <> Core_Cmp_Ordering_Type.C_Greater))
 end
 module CreusotContracts_Logic_Ord_Impl2_CmpLtLog_Stub
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  clone CreusotContracts_Logic_Ord_OrdLogic_LtLog_Stub as LtLog0 with
-    type self = Core_Option_Option_Type.t_option t
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  function cmp_lt_log (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
+  function cmp_lt_log (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
 end
 module CreusotContracts_Logic_Ord_Impl2_CmpLtLog_Interface
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  clone CreusotContracts_Logic_Ord_OrdLogic_LtLog_Stub as LtLog0 with
-    type self = Core_Option_Option_Type.t_option t
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  function cmp_lt_log (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
-  val cmp_lt_log (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 337 18 337 19] Inv0.inv x}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 337 27 337 28] Inv0.inv y}
-    ensures { [#"../../../../creusot-contracts/src/logic/ord.rs" 336 14 336 61] LtLog0.lt_log x y = (CmpLog0.cmp_log x y = Core_Cmp_Ordering_Type.C_Less) }
-    ensures { result = cmp_lt_log x y }
+  function cmp_lt_log (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
+  val cmp_lt_log (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
+    ensures { result = cmp_lt_log _1 _2 }
     
-  axiom cmp_lt_log_spec : forall x : Core_Option_Option_Type.t_option t, y : Core_Option_Option_Type.t_option t . ([#"../../../../creusot-contracts/src/logic/ord.rs" 337 18 337 19] Inv0.inv x) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 337 27 337 28] Inv0.inv y) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 336 14 336 61] LtLog0.lt_log x y = (CmpLog0.cmp_log x y = Core_Cmp_Ordering_Type.C_Less))
 end
 module CreusotContracts_Logic_Ord_Impl2_CmpLtLog
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  clone CreusotContracts_Logic_Ord_OrdLogic_LtLog_Stub as LtLog0 with
-    type self = Core_Option_Option_Type.t_option t
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  function cmp_lt_log (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : () =
-    [#"../../../../creusot-contracts/src/logic/ord.rs" 334 4 334 10] ()
-  val cmp_lt_log (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 337 18 337 19] Inv0.inv x}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 337 27 337 28] Inv0.inv y}
-    ensures { [#"../../../../creusot-contracts/src/logic/ord.rs" 336 14 336 61] LtLog0.lt_log x y = (CmpLog0.cmp_log x y = Core_Cmp_Ordering_Type.C_Less) }
-    ensures { result = cmp_lt_log x y }
+  function cmp_lt_log (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 85 12 85 14] ()
+  val cmp_lt_log (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
+    ensures { result = cmp_lt_log _1 _2 }
     
-  axiom cmp_lt_log_spec : forall x : Core_Option_Option_Type.t_option t, y : Core_Option_Option_Type.t_option t . ([#"../../../../creusot-contracts/src/logic/ord.rs" 337 18 337 19] Inv0.inv x) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 337 27 337 28] Inv0.inv y) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 336 14 336 61] LtLog0.lt_log x y = (CmpLog0.cmp_log x y = Core_Cmp_Ordering_Type.C_Less))
 end
 module CreusotContracts_Logic_Ord_Impl2_CmpGeLog_Stub
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  clone CreusotContracts_Logic_Ord_OrdLogic_GeLog_Stub as GeLog0 with
-    type self = Core_Option_Option_Type.t_option t
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  function cmp_ge_log (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
+  function cmp_ge_log (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
 end
 module CreusotContracts_Logic_Ord_Impl2_CmpGeLog_Interface
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  clone CreusotContracts_Logic_Ord_OrdLogic_GeLog_Stub as GeLog0 with
-    type self = Core_Option_Option_Type.t_option t
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  function cmp_ge_log (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
-  val cmp_ge_log (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 342 18 342 19] Inv0.inv x}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 342 27 342 28] Inv0.inv y}
-    ensures { [#"../../../../creusot-contracts/src/logic/ord.rs" 341 14 341 61] GeLog0.ge_log x y = (CmpLog0.cmp_log x y <> Core_Cmp_Ordering_Type.C_Less) }
-    ensures { result = cmp_ge_log x y }
+  function cmp_ge_log (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
+  val cmp_ge_log (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
+    ensures { result = cmp_ge_log _1 _2 }
     
-  axiom cmp_ge_log_spec : forall x : Core_Option_Option_Type.t_option t, y : Core_Option_Option_Type.t_option t . ([#"../../../../creusot-contracts/src/logic/ord.rs" 342 18 342 19] Inv0.inv x) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 342 27 342 28] Inv0.inv y) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 341 14 341 61] GeLog0.ge_log x y = (CmpLog0.cmp_log x y <> Core_Cmp_Ordering_Type.C_Less))
 end
 module CreusotContracts_Logic_Ord_Impl2_CmpGeLog
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  clone CreusotContracts_Logic_Ord_OrdLogic_GeLog_Stub as GeLog0 with
-    type self = Core_Option_Option_Type.t_option t
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  function cmp_ge_log (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : () =
-    [#"../../../../creusot-contracts/src/logic/ord.rs" 339 4 339 10] ()
-  val cmp_ge_log (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 342 18 342 19] Inv0.inv x}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 342 27 342 28] Inv0.inv y}
-    ensures { [#"../../../../creusot-contracts/src/logic/ord.rs" 341 14 341 61] GeLog0.ge_log x y = (CmpLog0.cmp_log x y <> Core_Cmp_Ordering_Type.C_Less) }
-    ensures { result = cmp_ge_log x y }
+  function cmp_ge_log (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 91 12 91 14] ()
+  val cmp_ge_log (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
+    ensures { result = cmp_ge_log _1 _2 }
     
-  axiom cmp_ge_log_spec : forall x : Core_Option_Option_Type.t_option t, y : Core_Option_Option_Type.t_option t . ([#"../../../../creusot-contracts/src/logic/ord.rs" 342 18 342 19] Inv0.inv x) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 342 27 342 28] Inv0.inv y) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 341 14 341 61] GeLog0.ge_log x y = (CmpLog0.cmp_log x y <> Core_Cmp_Ordering_Type.C_Less))
 end
 module CreusotContracts_Logic_Ord_Impl2_CmpGtLog_Stub
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  clone CreusotContracts_Logic_Ord_OrdLogic_GtLog_Stub as GtLog0 with
-    type self = Core_Option_Option_Type.t_option t
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  function cmp_gt_log (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
+  function cmp_gt_log (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
 end
 module CreusotContracts_Logic_Ord_Impl2_CmpGtLog_Interface
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  clone CreusotContracts_Logic_Ord_OrdLogic_GtLog_Stub as GtLog0 with
-    type self = Core_Option_Option_Type.t_option t
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  function cmp_gt_log (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
-  val cmp_gt_log (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 347 18 347 19] Inv0.inv x}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 347 27 347 28] Inv0.inv y}
-    ensures { [#"../../../../creusot-contracts/src/logic/ord.rs" 346 14 346 64] GtLog0.gt_log x y = (CmpLog0.cmp_log x y = Core_Cmp_Ordering_Type.C_Greater) }
-    ensures { result = cmp_gt_log x y }
+  function cmp_gt_log (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
+  val cmp_gt_log (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
+    ensures { result = cmp_gt_log _1 _2 }
     
-  axiom cmp_gt_log_spec : forall x : Core_Option_Option_Type.t_option t, y : Core_Option_Option_Type.t_option t . ([#"../../../../creusot-contracts/src/logic/ord.rs" 347 18 347 19] Inv0.inv x) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 347 27 347 28] Inv0.inv y) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 346 14 346 64] GtLog0.gt_log x y = (CmpLog0.cmp_log x y = Core_Cmp_Ordering_Type.C_Greater))
 end
 module CreusotContracts_Logic_Ord_Impl2_CmpGtLog
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  clone CreusotContracts_Logic_Ord_OrdLogic_GtLog_Stub as GtLog0 with
-    type self = Core_Option_Option_Type.t_option t
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  function cmp_gt_log (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : () =
-    [#"../../../../creusot-contracts/src/logic/ord.rs" 344 4 344 10] ()
-  val cmp_gt_log (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 347 18 347 19] Inv0.inv x}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 347 27 347 28] Inv0.inv y}
-    ensures { [#"../../../../creusot-contracts/src/logic/ord.rs" 346 14 346 64] GtLog0.gt_log x y = (CmpLog0.cmp_log x y = Core_Cmp_Ordering_Type.C_Greater) }
-    ensures { result = cmp_gt_log x y }
+  function cmp_gt_log (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 97 12 97 14] ()
+  val cmp_gt_log (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
+    ensures { result = cmp_gt_log _1 _2 }
     
-  axiom cmp_gt_log_spec : forall x : Core_Option_Option_Type.t_option t, y : Core_Option_Option_Type.t_option t . ([#"../../../../creusot-contracts/src/logic/ord.rs" 347 18 347 19] Inv0.inv x) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 347 27 347 28] Inv0.inv y) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 346 14 346 64] GtLog0.gt_log x y = (CmpLog0.cmp_log x y = Core_Cmp_Ordering_Type.C_Greater))
 end
 module CreusotContracts_Logic_Ord_Impl2_Refl_Stub
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  function refl (x : Core_Option_Option_Type.t_option t) : ()
+  function refl (_1 : Core_Option_Option_Type.t_option t) : ()
 end
 module CreusotContracts_Logic_Ord_Impl2_Refl_Interface
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  function refl (x : Core_Option_Option_Type.t_option t) : ()
-  val refl (x : Core_Option_Option_Type.t_option t) : ()
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 352 12 352 13] Inv0.inv x}
-    ensures { [#"../../../../creusot-contracts/src/logic/ord.rs" 351 14 351 45] CmpLog0.cmp_log x x = Core_Cmp_Ordering_Type.C_Equal }
-    ensures { result = refl x }
+  function refl (_1 : Core_Option_Option_Type.t_option t) : ()
+  val refl (_1 : Core_Option_Option_Type.t_option t) : ()
+    ensures { result = refl _1 }
     
-  axiom refl_spec : forall x : Core_Option_Option_Type.t_option t . ([#"../../../../creusot-contracts/src/logic/ord.rs" 352 12 352 13] Inv0.inv x) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 351 14 351 45] CmpLog0.cmp_log x x = Core_Cmp_Ordering_Type.C_Equal)
 end
 module CreusotContracts_Logic_Ord_Impl2_Refl
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  function refl (x : Core_Option_Option_Type.t_option t) : () =
-    [#"../../../../creusot-contracts/src/logic/ord.rs" 349 4 349 10] ()
-  val refl (x : Core_Option_Option_Type.t_option t) : ()
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 352 12 352 13] Inv0.inv x}
-    ensures { [#"../../../../creusot-contracts/src/logic/ord.rs" 351 14 351 45] CmpLog0.cmp_log x x = Core_Cmp_Ordering_Type.C_Equal }
-    ensures { result = refl x }
+  function refl (_1 : Core_Option_Option_Type.t_option t) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 103 12 103 14] ()
+  val refl (_1 : Core_Option_Option_Type.t_option t) : ()
+    ensures { result = refl _1 }
     
-  axiom refl_spec : forall x : Core_Option_Option_Type.t_option t . ([#"../../../../creusot-contracts/src/logic/ord.rs" 352 12 352 13] Inv0.inv x) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 351 14 351 45] CmpLog0.cmp_log x x = Core_Cmp_Ordering_Type.C_Equal)
 end
 module CreusotContracts_Logic_Ord_Impl2_Trans_Stub
   type t
   use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
   use Core_Option_Option_Type as Core_Option_Option_Type
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  function trans (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) (z : Core_Option_Option_Type.t_option t) (o : Core_Cmp_Ordering_Type.t_ordering) : ()
+  function trans (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) (_3 : Core_Option_Option_Type.t_option t) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
     
 end
 module CreusotContracts_Logic_Ord_Impl2_Trans_Interface
   type t
   use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
   use Core_Option_Option_Type as Core_Option_Option_Type
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  function trans (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) (z : Core_Option_Option_Type.t_option t) (o : Core_Cmp_Ordering_Type.t_ordering) : ()
-    
-  val trans (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) (z : Core_Option_Option_Type.t_option t) (o : Core_Cmp_Ordering_Type.t_ordering) : ()
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 356 15 356 32] CmpLog0.cmp_log x y = o}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 357 15 357 32] CmpLog0.cmp_log y z = o}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 359 13 359 14] Inv0.inv x}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 359 22 359 23] Inv0.inv y}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 359 31 359 32] Inv0.inv z}
-    ensures { [#"../../../../creusot-contracts/src/logic/ord.rs" 358 14 358 31] CmpLog0.cmp_log x z = o }
-    ensures { result = trans x y z o }
+  function trans (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) (_3 : Core_Option_Option_Type.t_option t) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+    
+  val trans (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) (_3 : Core_Option_Option_Type.t_option t) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+    ensures { result = trans _1 _2 _3 _4 }
     
-  axiom trans_spec : forall x : Core_Option_Option_Type.t_option t, y : Core_Option_Option_Type.t_option t, z : Core_Option_Option_Type.t_option t, o : Core_Cmp_Ordering_Type.t_ordering . ([#"../../../../creusot-contracts/src/logic/ord.rs" 356 15 356 32] CmpLog0.cmp_log x y = o) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 357 15 357 32] CmpLog0.cmp_log y z = o) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 359 13 359 14] Inv0.inv x) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 359 22 359 23] Inv0.inv y) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 359 31 359 32] Inv0.inv z) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 358 14 358 31] CmpLog0.cmp_log x z = o)
 end
 module CreusotContracts_Logic_Ord_Impl2_Trans
   type t
   use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
   use Core_Option_Option_Type as Core_Option_Option_Type
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  function trans (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) (z : Core_Option_Option_Type.t_option t) (o : Core_Cmp_Ordering_Type.t_ordering) : ()
+  function trans (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) (_3 : Core_Option_Option_Type.t_option t) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
     
    =
-    [#"../../../../creusot-contracts/src/logic/ord.rs" 354 4 354 10] ()
-  val trans (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) (z : Core_Option_Option_Type.t_option t) (o : Core_Cmp_Ordering_Type.t_ordering) : ()
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 356 15 356 32] CmpLog0.cmp_log x y = o}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 357 15 357 32] CmpLog0.cmp_log y z = o}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 359 13 359 14] Inv0.inv x}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 359 22 359 23] Inv0.inv y}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 359 31 359 32] Inv0.inv z}
-    ensures { [#"../../../../creusot-contracts/src/logic/ord.rs" 358 14 358 31] CmpLog0.cmp_log x z = o }
-    ensures { result = trans x y z o }
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 109 12 109 14] ()
+  val trans (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) (_3 : Core_Option_Option_Type.t_option t) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+    ensures { result = trans _1 _2 _3 _4 }
     
-  axiom trans_spec : forall x : Core_Option_Option_Type.t_option t, y : Core_Option_Option_Type.t_option t, z : Core_Option_Option_Type.t_option t, o : Core_Cmp_Ordering_Type.t_ordering . ([#"../../../../creusot-contracts/src/logic/ord.rs" 356 15 356 32] CmpLog0.cmp_log x y = o) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 357 15 357 32] CmpLog0.cmp_log y z = o) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 359 13 359 14] Inv0.inv x) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 359 22 359 23] Inv0.inv y) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 359 31 359 32] Inv0.inv z) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 358 14 358 31] CmpLog0.cmp_log x z = o)
 end
 module CreusotContracts_Logic_Ord_Impl2_Antisym1_Stub
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  function antisym1 (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
+  function antisym1 (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
 end
 module CreusotContracts_Logic_Ord_Impl2_Antisym1_Interface
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  function antisym1 (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
-  val antisym1 (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 363 15 363 45] CmpLog0.cmp_log x y = Core_Cmp_Ordering_Type.C_Less}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 365 16 365 17] Inv0.inv x}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 365 25 365 26] Inv0.inv y}
-    ensures { [#"../../../../creusot-contracts/src/logic/ord.rs" 364 14 364 47] CmpLog0.cmp_log y x = Core_Cmp_Ordering_Type.C_Greater }
-    ensures { result = antisym1 x y }
+  function antisym1 (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
+  val antisym1 (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
+    ensures { result = antisym1 _1 _2 }
     
-  axiom antisym1_spec : forall x : Core_Option_Option_Type.t_option t, y : Core_Option_Option_Type.t_option t . ([#"../../../../creusot-contracts/src/logic/ord.rs" 363 15 363 45] CmpLog0.cmp_log x y = Core_Cmp_Ordering_Type.C_Less) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 365 16 365 17] Inv0.inv x) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 365 25 365 26] Inv0.inv y) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 364 14 364 47] CmpLog0.cmp_log y x = Core_Cmp_Ordering_Type.C_Greater)
 end
 module CreusotContracts_Logic_Ord_Impl2_Antisym1
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  function antisym1 (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : () =
-    [#"../../../../creusot-contracts/src/logic/ord.rs" 361 4 361 10] ()
-  val antisym1 (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 363 15 363 45] CmpLog0.cmp_log x y = Core_Cmp_Ordering_Type.C_Less}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 365 16 365 17] Inv0.inv x}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 365 25 365 26] Inv0.inv y}
-    ensures { [#"../../../../creusot-contracts/src/logic/ord.rs" 364 14 364 47] CmpLog0.cmp_log y x = Core_Cmp_Ordering_Type.C_Greater }
-    ensures { result = antisym1 x y }
+  function antisym1 (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 115 12 115 14] ()
+  val antisym1 (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
+    ensures { result = antisym1 _1 _2 }
     
-  axiom antisym1_spec : forall x : Core_Option_Option_Type.t_option t, y : Core_Option_Option_Type.t_option t . ([#"../../../../creusot-contracts/src/logic/ord.rs" 363 15 363 45] CmpLog0.cmp_log x y = Core_Cmp_Ordering_Type.C_Less) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 365 16 365 17] Inv0.inv x) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 365 25 365 26] Inv0.inv y) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 364 14 364 47] CmpLog0.cmp_log y x = Core_Cmp_Ordering_Type.C_Greater)
 end
 module CreusotContracts_Logic_Ord_Impl2_Antisym2_Stub
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  function antisym2 (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
+  function antisym2 (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
 end
 module CreusotContracts_Logic_Ord_Impl2_Antisym2_Interface
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  function antisym2 (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
-  val antisym2 (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 369 15 369 48] CmpLog0.cmp_log x y = Core_Cmp_Ordering_Type.C_Greater}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 371 16 371 17] Inv0.inv x}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 371 25 371 26] Inv0.inv y}
-    ensures { [#"../../../../creusot-contracts/src/logic/ord.rs" 370 14 370 44] CmpLog0.cmp_log y x = Core_Cmp_Ordering_Type.C_Less }
-    ensures { result = antisym2 x y }
+  function antisym2 (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
+  val antisym2 (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
+    ensures { result = antisym2 _1 _2 }
     
-  axiom antisym2_spec : forall x : Core_Option_Option_Type.t_option t, y : Core_Option_Option_Type.t_option t . ([#"../../../../creusot-contracts/src/logic/ord.rs" 369 15 369 48] CmpLog0.cmp_log x y = Core_Cmp_Ordering_Type.C_Greater) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 371 16 371 17] Inv0.inv x) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 371 25 371 26] Inv0.inv y) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 370 14 370 44] CmpLog0.cmp_log y x = Core_Cmp_Ordering_Type.C_Less)
 end
 module CreusotContracts_Logic_Ord_Impl2_Antisym2
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  function antisym2 (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : () =
-    [#"../../../../creusot-contracts/src/logic/ord.rs" 367 4 367 10] ()
-  val antisym2 (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 369 15 369 48] CmpLog0.cmp_log x y = Core_Cmp_Ordering_Type.C_Greater}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 371 16 371 17] Inv0.inv x}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 371 25 371 26] Inv0.inv y}
-    ensures { [#"../../../../creusot-contracts/src/logic/ord.rs" 370 14 370 44] CmpLog0.cmp_log y x = Core_Cmp_Ordering_Type.C_Less }
-    ensures { result = antisym2 x y }
+  function antisym2 (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 121 12 121 14] ()
+  val antisym2 (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
+    ensures { result = antisym2 _1 _2 }
     
-  axiom antisym2_spec : forall x : Core_Option_Option_Type.t_option t, y : Core_Option_Option_Type.t_option t . ([#"../../../../creusot-contracts/src/logic/ord.rs" 369 15 369 48] CmpLog0.cmp_log x y = Core_Cmp_Ordering_Type.C_Greater) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 371 16 371 17] Inv0.inv x) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 371 25 371 26] Inv0.inv y) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 370 14 370 44] CmpLog0.cmp_log y x = Core_Cmp_Ordering_Type.C_Less)
 end
 module CreusotContracts_Logic_Ord_Impl2_EqCmp_Stub
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  function eq_cmp (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
+  function eq_cmp (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
 end
 module CreusotContracts_Logic_Ord_Impl2_EqCmp_Interface
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  function eq_cmp (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
-  val eq_cmp (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 376 14 376 15] Inv0.inv x}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 376 23 376 24] Inv0.inv y}
-    ensures { [#"../../../../creusot-contracts/src/logic/ord.rs" 375 14 375 59] (x = y) = (CmpLog0.cmp_log x y = Core_Cmp_Ordering_Type.C_Equal) }
-    ensures { result = eq_cmp x y }
+  function eq_cmp (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
+  val eq_cmp (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
+    ensures { result = eq_cmp _1 _2 }
     
-  axiom eq_cmp_spec : forall x : Core_Option_Option_Type.t_option t, y : Core_Option_Option_Type.t_option t . ([#"../../../../creusot-contracts/src/logic/ord.rs" 376 14 376 15] Inv0.inv x) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 376 23 376 24] Inv0.inv y) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 375 14 375 59] (x = y) = (CmpLog0.cmp_log x y = Core_Cmp_Ordering_Type.C_Equal))
 end
 module CreusotContracts_Logic_Ord_Impl2_EqCmp
   type t
   use Core_Option_Option_Type as Core_Option_Option_Type
-  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLog_Stub as CmpLog0 with
-    type t = t
-  clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
-    type t = Core_Option_Option_Type.t_option t
-  function eq_cmp (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : () =
-    [#"../../../../creusot-contracts/src/logic/ord.rs" 373 4 373 10] ()
-  val eq_cmp (x : Core_Option_Option_Type.t_option t) (y : Core_Option_Option_Type.t_option t) : ()
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 376 14 376 15] Inv0.inv x}
-    requires {[#"../../../../creusot-contracts/src/logic/ord.rs" 376 23 376 24] Inv0.inv y}
-    ensures { [#"../../../../creusot-contracts/src/logic/ord.rs" 375 14 375 59] (x = y) = (CmpLog0.cmp_log x y = Core_Cmp_Ordering_Type.C_Equal) }
-    ensures { result = eq_cmp x y }
+  function eq_cmp (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 127 12 127 14] ()
+  val eq_cmp (_1 : Core_Option_Option_Type.t_option t) (_2 : Core_Option_Option_Type.t_option t) : ()
+    ensures { result = eq_cmp _1 _2 }
     
-  axiom eq_cmp_spec : forall x : Core_Option_Option_Type.t_option t, y : Core_Option_Option_Type.t_option t . ([#"../../../../creusot-contracts/src/logic/ord.rs" 376 14 376 15] Inv0.inv x) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 376 23 376 24] Inv0.inv y) -> ([#"../../../../creusot-contracts/src/logic/ord.rs" 375 14 375 59] (x = y) = (CmpLog0.cmp_log x y = Core_Cmp_Ordering_Type.C_Equal))
 end
 module CreusotContracts_Logic_Ord_Impl3_CmpLog_Stub
   use prelude.Int
@@ -1759,7 +1697,7 @@ module CreusotContracts_Logic_Ord_Impl3_CmpLog
   use prelude.Int
   use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
   function cmp_log (self : int) (o : int) : Core_Cmp_Ordering_Type.t_ordering =
-    [#"../../../../creusot-contracts/src/logic/ord.rs" 76 12 85 17] if self < o then
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 137 12 146 17] if self < o then
       Core_Cmp_Ordering_Type.C_Less
     else
       if self = o then Core_Cmp_Ordering_Type.C_Equal else Core_Cmp_Ordering_Type.C_Greater
@@ -1785,70 +1723,33 @@ module Instant_TestInstant
     axiom .
   use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
   clone CreusotContracts_Logic_Ord_Impl3_CmpLog as CmpLog1
+  clone CreusotContracts_Logic_Ord_Impl2_EqCmp_Interface as EqCmp2 with
+    type t = int
+  clone CreusotContracts_Logic_Ord_Impl2_Antisym2_Interface as Antisym22 with
+    type t = int
+  clone CreusotContracts_Logic_Ord_Impl2_Antisym1_Interface as Antisym12 with
+    type t = int
+  clone CreusotContracts_Logic_Ord_Impl2_Trans_Interface as Trans2 with
+    type t = int
+  clone CreusotContracts_Logic_Ord_Impl2_Refl_Interface as Refl2 with
+    type t = int
+  clone CreusotContracts_Logic_Ord_Impl2_CmpGtLog_Interface as CmpGtLog2 with
+    type t = int
+  clone CreusotContracts_Logic_Ord_Impl2_CmpGeLog_Interface as CmpGeLog2 with
+    type t = int
+  clone CreusotContracts_Logic_Ord_Impl2_CmpLtLog_Interface as CmpLtLog2 with
+    type t = int
+  clone CreusotContracts_Logic_Ord_Impl2_CmpLeLog_Interface as CmpLeLog2 with
+    type t = int
   clone CreusotContracts_Logic_Ord_Impl2_CmpLog as CmpLog0 with
     type t = int,
     function CmpLog0.cmp_log = CmpLog1.cmp_log
-  clone CreusotContracts_Logic_Ord_Impl2_EqCmp_Interface as EqCmp1 with
-    type t = int,
-    predicate Inv0.inv = Inv4.inv,
-    function CmpLog0.cmp_log = CmpLog0.cmp_log,
-    axiom .
-  clone CreusotContracts_Logic_Ord_Impl2_Antisym2_Interface as Antisym21 with
-    type t = int,
-    function CmpLog0.cmp_log = CmpLog0.cmp_log,
-    predicate Inv0.inv = Inv4.inv,
-    axiom .
-  clone CreusotContracts_Logic_Ord_Impl2_Antisym1_Interface as Antisym11 with
-    type t = int,
-    function CmpLog0.cmp_log = CmpLog0.cmp_log,
-    predicate Inv0.inv = Inv4.inv,
-    axiom .
-  clone CreusotContracts_Logic_Ord_Impl2_Trans_Interface as Trans1 with
-    type t = int,
-    function CmpLog0.cmp_log = CmpLog0.cmp_log,
-    predicate Inv0.inv = Inv4.inv,
-    axiom .
-  clone CreusotContracts_Logic_Ord_Impl2_Refl_Interface as Refl1 with
-    type t = int,
-    predicate Inv0.inv = Inv4.inv,
-    function CmpLog0.cmp_log = CmpLog0.cmp_log,
-    axiom .
-  clone CreusotContracts_Logic_Ord_OrdLogic_GtLog as GtLog0 with
-    type self = Core_Option_Option_Type.t_option int,
-    function CmpLog0.cmp_log = CmpLog0.cmp_log
-  clone CreusotContracts_Logic_Ord_Impl2_CmpGtLog_Interface as CmpGtLog1 with
-    type t = int,
-    predicate Inv0.inv = Inv4.inv,
-    function GtLog0.gt_log = GtLog0.gt_log,
-    function CmpLog0.cmp_log = CmpLog0.cmp_log,
-    axiom .
   clone CreusotContracts_Logic_Ord_OrdLogic_GeLog as GeLog1 with
     type self = Core_Option_Option_Type.t_option int,
     function CmpLog0.cmp_log = CmpLog0.cmp_log
-  clone CreusotContracts_Logic_Ord_Impl2_CmpGeLog_Interface as CmpGeLog1 with
-    type t = int,
-    predicate Inv0.inv = Inv4.inv,
-    function GeLog0.ge_log = GeLog1.ge_log,
-    function CmpLog0.cmp_log = CmpLog0.cmp_log,
-    axiom .
-  clone CreusotContracts_Logic_Ord_OrdLogic_LtLog as LtLog0 with
-    type self = Core_Option_Option_Type.t_option int,
-    function CmpLog0.cmp_log = CmpLog0.cmp_log
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLtLog_Interface as CmpLtLog1 with
-    type t = int,
-    predicate Inv0.inv = Inv4.inv,
-    function LtLog0.lt_log = LtLog0.lt_log,
-    function CmpLog0.cmp_log = CmpLog0.cmp_log,
-    axiom .
   clone CreusotContracts_Logic_Ord_OrdLogic_LeLog as LeLog0 with
     type self = Core_Option_Option_Type.t_option int,
     function CmpLog0.cmp_log = CmpLog0.cmp_log
-  clone CreusotContracts_Logic_Ord_Impl2_CmpLeLog_Interface as CmpLeLog1 with
-    type t = int,
-    predicate Inv0.inv = Inv4.inv,
-    function LeLog0.le_log = LeLog0.le_log,
-    function CmpLog0.cmp_log = CmpLog0.cmp_log,
-    axiom .
   use Core_Time_Duration_Type as Core_Time_Duration_Type
   clone CreusotContracts_Invariant_Inv_Interface as Inv3 with
     type t = Core_Option_Option_Type.t_option (Core_Time_Duration_Type.t_duration)
@@ -1869,50 +1770,56 @@ module Instant_TestInstant
     type t = Core_Option_Option_Type.t_option (Std_Time_Instant_Type.t_instant),
     predicate Inv0.inv = Inv1.inv,
     axiom .
-  clone CreusotContracts_Logic_Ord_OrdLogic_EqCmp_Interface as EqCmp0 with
+  clone CreusotContracts_Logic_Ord_OrdLogic_EqCmp_Interface as EqCmp1 with
     type self = Core_Option_Option_Type.t_option int,
     predicate Inv0.inv = Inv4.inv,
     function CmpLog0.cmp_log = CmpLog0.cmp_log,
     axiom .
-  clone CreusotContracts_Logic_Ord_OrdLogic_Antisym2_Interface as Antisym20 with
+  clone CreusotContracts_Logic_Ord_OrdLogic_Antisym2_Interface as Antisym21 with
     type self = Core_Option_Option_Type.t_option int,
     function CmpLog0.cmp_log = CmpLog0.cmp_log,
     predicate Inv0.inv = Inv4.inv,
     axiom .
-  clone CreusotContracts_Logic_Ord_OrdLogic_Antisym1_Interface as Antisym10 with
+  clone CreusotContracts_Logic_Ord_OrdLogic_Antisym1_Interface as Antisym11 with
     type self = Core_Option_Option_Type.t_option int,
     function CmpLog0.cmp_log = CmpLog0.cmp_log,
     predicate Inv0.inv = Inv4.inv,
     axiom .
-  clone CreusotContracts_Logic_Ord_OrdLogic_Trans_Interface as Trans0 with
+  clone CreusotContracts_Logic_Ord_OrdLogic_Trans_Interface as Trans1 with
     type self = Core_Option_Option_Type.t_option int,
     function CmpLog0.cmp_log = CmpLog0.cmp_log,
     predicate Inv0.inv = Inv4.inv,
     axiom .
-  clone CreusotContracts_Logic_Ord_OrdLogic_Refl_Interface as Refl0 with
+  clone CreusotContracts_Logic_Ord_OrdLogic_Refl_Interface as Refl1 with
     type self = Core_Option_Option_Type.t_option int,
     predicate Inv0.inv = Inv4.inv,
     function CmpLog0.cmp_log = CmpLog0.cmp_log,
     axiom .
-  clone CreusotContracts_Logic_Ord_OrdLogic_CmpGtLog_Interface as CmpGtLog0 with
+  clone CreusotContracts_Logic_Ord_OrdLogic_GtLog as GtLog0 with
+    type self = Core_Option_Option_Type.t_option int,
+    function CmpLog0.cmp_log = CmpLog0.cmp_log
+  clone CreusotContracts_Logic_Ord_OrdLogic_CmpGtLog_Interface as CmpGtLog1 with
     type self = Core_Option_Option_Type.t_option int,
     predicate Inv0.inv = Inv4.inv,
     function GtLog0.gt_log = GtLog0.gt_log,
     function CmpLog0.cmp_log = CmpLog0.cmp_log,
     axiom .
-  clone CreusotContracts_Logic_Ord_OrdLogic_CmpGeLog_Interface as CmpGeLog0 with
+  clone CreusotContracts_Logic_Ord_OrdLogic_CmpGeLog_Interface as CmpGeLog1 with
     type self = Core_Option_Option_Type.t_option int,
     predicate Inv0.inv = Inv4.inv,
     function GeLog0.ge_log = GeLog1.ge_log,
     function CmpLog0.cmp_log = CmpLog0.cmp_log,
     axiom .
-  clone CreusotContracts_Logic_Ord_OrdLogic_CmpLtLog_Interface as CmpLtLog0 with
+  clone CreusotContracts_Logic_Ord_OrdLogic_LtLog as LtLog0 with
+    type self = Core_Option_Option_Type.t_option int,
+    function CmpLog0.cmp_log = CmpLog0.cmp_log
+  clone CreusotContracts_Logic_Ord_OrdLogic_CmpLtLog_Interface as CmpLtLog1 with
     type self = Core_Option_Option_Type.t_option int,
     predicate Inv0.inv = Inv4.inv,
     function LtLog0.lt_log = LtLog0.lt_log,
     function CmpLog0.cmp_log = CmpLog0.cmp_log,
     axiom .
-  clone CreusotContracts_Logic_Ord_OrdLogic_CmpLeLog_Interface as CmpLeLog0 with
+  clone CreusotContracts_Logic_Ord_OrdLogic_CmpLeLog_Interface as CmpLeLog1 with
     type self = Core_Option_Option_Type.t_option int,
     predicate Inv0.inv = Inv4.inv,
     function LeLog0.le_log = LeLog0.le_log,
@@ -1923,6 +1830,15 @@ module Instant_TestInstant
   clone CreusotContracts_Std1_Time_Impl3_DeepModel_Interface as DeepModel4 with
     function ShallowModel0.shallow_model = ShallowModel0.shallow_model,
     axiom .
+  clone CreusotContracts_Logic_Ord_Impl3_EqCmp_Interface as EqCmp0
+  clone CreusotContracts_Logic_Ord_Impl3_Antisym2_Interface as Antisym20
+  clone CreusotContracts_Logic_Ord_Impl3_Antisym1_Interface as Antisym10
+  clone CreusotContracts_Logic_Ord_Impl3_Trans_Interface as Trans0
+  clone CreusotContracts_Logic_Ord_Impl3_Refl_Interface as Refl0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Interface as CmpGtLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Interface as CmpGeLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Interface as CmpLtLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Interface as CmpLeLog0
   clone CreusotContracts_Std1_Time_SecsToNanos_Interface as SecsToNanos0
   clone Core_Num_Impl9_Max as Max0
   clone CreusotContracts_Std1_Time_Impl0_ShallowModel_Interface as ShallowModel1 with
diff --git a/creusot/tests/should_succeed/knapsack_full.mlcfg b/creusot/tests/should_succeed/knapsack_full.mlcfg
index a23606dbcf..f831d8841a 100644
--- a/creusot/tests/should_succeed/knapsack_full.mlcfg
+++ b/creusot/tests/should_succeed/knapsack_full.mlcfg
@@ -2122,6 +2122,180 @@ module CreusotContracts_Std1_Slice_Impl5_ResolveElswhere
   val resolve_elswhere [@inline:trivial] (self : usize) (old' : Seq.seq t) (fin : Seq.seq t) : bool
     ensures { result = resolve_elswhere self old' fin }
     
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Stub
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Interface
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : ()
+  val cmp_le_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_le_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 79 12 79 14] ()
+  val cmp_le_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_le_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Stub
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Interface
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : ()
+  val cmp_lt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_lt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 85 12 85 14] ()
+  val cmp_lt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_lt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Stub
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Interface
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : ()
+  val cmp_ge_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_ge_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 91 12 91 14] ()
+  val cmp_ge_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_ge_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Stub
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Interface
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : ()
+  val cmp_gt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_gt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 97 12 97 14] ()
+  val cmp_gt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_gt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl_Stub
+  use prelude.Int
+  function refl (_1 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl_Interface
+  use prelude.Int
+  function refl (_1 : int) : ()
+  val refl (_1 : int) : ()
+    ensures { result = refl _1 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl
+  use prelude.Int
+  function refl (_1 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 103 12 103 14] ()
+  val refl (_1 : int) : ()
+    ensures { result = refl _1 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans_Stub
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans_Interface
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+  val trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+    ensures { result = trans _1 _2 _3 _4 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 109 12 109 14] ()
+  val trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+    ensures { result = trans _1 _2 _3 _4 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1_Stub
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1_Interface
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : ()
+  val antisym1 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym1 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 115 12 115 14] ()
+  val antisym1 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym1 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2_Stub
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2_Interface
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : ()
+  val antisym2 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym2 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 121 12 121 14] ()
+  val antisym2 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym2 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp_Stub
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp_Interface
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : ()
+  val eq_cmp (_1 : int) (_2 : int) : ()
+    ensures { result = eq_cmp _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 127 12 127 14] ()
+  val eq_cmp (_1 : int) (_2 : int) : ()
+    ensures { result = eq_cmp _1 _2 }
+    
 end
 module CreusotContracts_Resolve_Impl2_Resolve_Stub
   type t
@@ -2200,6 +2374,7 @@ module KnapsackFull_Knapsack01Dyn
   use prelude.Ghost
   use seq.Seq
   use prelude.Borrow
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
   use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
   use KnapsackFull_Item_Type as KnapsackFull_Item_Type
   use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
@@ -2260,6 +2435,15 @@ module KnapsackFull_Knapsack01Dyn
     type t = borrowed (Core_Ops_Range_RangeInclusive_Type.t_rangeinclusive usize),
     predicate Inv0.inv = Inv14.inv,
     axiom .
+  clone CreusotContracts_Logic_Ord_Impl3_EqCmp_Interface as EqCmp0
+  clone CreusotContracts_Logic_Ord_Impl3_Antisym2_Interface as Antisym20
+  clone CreusotContracts_Logic_Ord_Impl3_Antisym1_Interface as Antisym10
+  clone CreusotContracts_Logic_Ord_Impl3_Trans_Interface as Trans0
+  clone CreusotContracts_Logic_Ord_Impl3_Refl_Interface as Refl0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Interface as CmpGtLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Interface as CmpGeLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Interface as CmpLtLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Interface as CmpLeLog0
   use Core_Option_Option_Type as Core_Option_Option_Type
   clone CreusotContracts_Invariant_Inv_Interface as Inv13 with
     type t = Core_Option_Option_Type.t_option usize
diff --git a/creusot/tests/should_succeed/knapsack_full/why3session.xml b/creusot/tests/should_succeed/knapsack_full/why3session.xml
index e7950c42b7..83eeaddb47 100644
--- a/creusot/tests/should_succeed/knapsack_full/why3session.xml
+++ b/creusot/tests/should_succeed/knapsack_full/why3session.xml
@@ -38,22 +38,22 @@
  <goal name="knapsack01_dyn&#39;vc" expl="VC for knapsack01_dyn" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="knapsack01_dyn&#39;vc.0" expl="integer overflow" proved="true">
-  <proof prover="5"><result status="valid" time="0.011401" steps="15"/></proof>
+  <proof prover="5"><result status="valid" time="0.011401" steps="14"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.1" expl="precondition" proved="true">
   <proof prover="5"><result status="valid" time="0.014143" steps="22"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.2" expl="precondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.020097" steps="17"/></proof>
+  <proof prover="5"><result status="valid" time="0.020097" steps="16"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.3" expl="integer overflow" proved="true">
-  <proof prover="5"><result status="valid" time="0.012163" steps="41"/></proof>
+  <proof prover="5"><result status="valid" time="0.012163" steps="40"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.4" expl="precondition" proved="true">
   <proof prover="5"><result status="valid" time="0.017609" steps="22"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.5" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.039289" steps="11985"/></proof>
+  <proof prover="1"><result status="valid" time="0.039289" steps="11985"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.6" expl="precondition" proved="true">
   <proof prover="5"><result status="valid" time="0.011043" steps="29"/></proof>
@@ -62,7 +62,7 @@
   <proof prover="5"><result status="valid" time="0.014713" steps="53"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.8" expl="loop invariant init" proved="true">
-  <proof prover="3"><result status="valid" time="0.011373" steps="12342"/></proof>
+  <proof prover="1"><result status="valid" time="0.011373" steps="12342"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.9" expl="loop invariant init" proved="true">
   <proof prover="5"><result status="valid" time="0.013632" steps="65"/></proof>
@@ -71,19 +71,19 @@
   <proof prover="5"><result status="valid" time="0.011336" steps="36"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.11" expl="loop invariant init" proved="true">
-  <proof prover="5"><result status="valid" time="0.013452" steps="71"/></proof>
+  <proof prover="5"><result status="valid" time="0.013452" steps="70"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.12" expl="loop invariant init" proved="true">
-  <proof prover="5"><result status="valid" time="0.024395" steps="343"/></proof>
+  <proof prover="5"><result status="valid" time="0.024395" steps="342"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.13" expl="loop invariant init" proved="true">
-  <proof prover="5"><result status="valid" time="0.018805" steps="173"/></proof>
+  <proof prover="5"><result status="valid" time="0.018805" steps="172"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.14" expl="precondition" proved="true">
   <proof prover="5"><result status="valid" time="0.016312" steps="75"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.15" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.046646" steps="12710"/></proof>
+  <proof prover="1"><result status="valid" time="0.046646" steps="12704"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.16" expl="precondition" proved="true">
   <proof prover="5"><result status="valid" time="0.015268" steps="62"/></proof>
@@ -98,13 +98,13 @@
   <proof prover="5"><result status="valid" time="0.012916" steps="72"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.20" expl="loop invariant init" proved="true">
-  <proof prover="3"><result status="valid" time="0.019851" steps="82469"/></proof>
+  <proof prover="1"><result status="valid" time="0.019851" steps="101365"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.21" expl="loop invariant init" proved="true">
   <proof prover="5"><result status="valid" time="0.013177" steps="72"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.22" expl="integer overflow" proved="true">
-  <proof prover="5"><result status="valid" time="0.016048" steps="116"/></proof>
+  <proof prover="5"><result status="valid" time="0.016048" steps="115"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.23" expl="precondition" proved="true">
   <proof prover="5"><result status="valid" time="0.013470" steps="72"/></proof>
@@ -125,19 +125,19 @@
   <proof prover="5"><result status="valid" time="0.013380" steps="82"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.29" expl="precondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.014239" steps="144"/></proof>
+  <proof prover="5"><result status="valid" time="0.014239" steps="143"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.30" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.032819" steps="173959"/></proof>
+  <proof prover="1"><result status="valid" time="0.032819" steps="193436"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.31" expl="precondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.018504" steps="181"/></proof>
+  <proof prover="5"><result status="valid" time="0.018504" steps="161"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.32" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.127437" steps="13245"/></proof>
+  <proof prover="1"><result status="valid" time="0.011539" steps="13239"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.33" expl="precondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.018515" steps="155"/></proof>
+  <proof prover="5"><result status="valid" time="0.018515" steps="153"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.34" expl="precondition" proved="true">
   <proof prover="5"><result status="valid" time="0.013700" steps="90"/></proof>
@@ -146,16 +146,16 @@
   <proof prover="5"><result status="valid" time="0.012814" steps="160"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.36" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.031382" steps="174472"/></proof>
+  <proof prover="1"><result status="valid" time="0.031382" steps="193983"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.37" expl="precondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.019570" steps="196"/></proof>
+  <proof prover="5"><result status="valid" time="0.019570" steps="175"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.38" expl="precondition" proved="true">
   <proof prover="5"><result status="valid" time="0.021841" steps="96"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.39" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.036002" steps="174729"/></proof>
+  <proof prover="1"><result status="valid" time="0.036002" steps="194257"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.40" expl="type invariant" proved="true">
   <proof prover="5"><result status="valid" time="0.014931" steps="100"/></proof>
@@ -164,52 +164,52 @@
   <proof prover="5"><result status="valid" time="0.014302" steps="209"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.42" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.024479" steps="46628"/></proof>
+  <proof prover="1"><result status="valid" time="0.024479" steps="105244"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.43" expl="type invariant" proved="true">
   <proof prover="5"><result status="valid" time="0.025140" steps="108"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.44" expl="integer overflow" proved="true">
-  <proof prover="3"><result status="valid" time="0.491392" steps="853182"/></proof>
+  <proof prover="1"><result status="valid" time="0.113641" steps="619031"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.45" expl="type invariant" proved="true">
   <proof prover="5"><result status="valid" time="0.017596" steps="72"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.46" expl="postcondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.061701" steps="706"/></proof>
+  <proof prover="5"><result status="valid" time="0.061701" steps="703"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.47" expl="postcondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.177099" steps="420756"/></proof>
+  <proof prover="1"><result status="valid" time="0.177099" steps="440283"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.48" expl="postcondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.035419" steps="176143"/></proof>
+  <proof prover="1"><result status="valid" time="0.035419" steps="195734"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.49" expl="postcondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.036480" steps="131"/></proof>
+  <proof prover="5"><result status="valid" time="0.036480" steps="128"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.50" expl="loop invariant preservation" proved="true">
   <proof prover="5"><result status="valid" time="0.020488" steps="100"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.51" expl="loop invariant preservation" proved="true">
-  <proof prover="5"><result status="valid" time="0.024641" steps="320"/></proof>
+  <proof prover="5"><result status="valid" time="0.024641" steps="318"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.52" expl="loop invariant preservation" proved="true">
-  <proof prover="3"><result status="valid" time="0.646364" steps="1187327"/></proof>
+  <proof prover="1"><result status="valid" time="0.398416" steps="2195538"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.53" expl="loop invariant preservation" proved="true">
-  <proof prover="3"><result status="valid" time="1.681631" steps="6516268"/></proof>
+  <proof prover="1"><result status="valid" time="0.222101" steps="1356796"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.54" expl="loop invariant preservation" proved="true">
-  <proof prover="3"><result status="valid" time="0.984757" steps="1386013"/></proof>
+  <proof prover="1"><result status="valid" time="0.474101" steps="1882707"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.55" expl="precondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.152463" steps="516"/></proof>
+  <proof prover="5"><result status="valid" time="0.032376" steps="514"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.56" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.039703" steps="12795"/></proof>
+  <proof prover="1"><result status="valid" time="0.039703" steps="12789"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.57" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.011525" steps="161986"/></proof>
+  <proof prover="1"><result status="valid" time="0.011525" steps="180822"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.58" expl="type invariant" proved="true">
   <proof prover="5"><result status="valid" time="0.014203" steps="72"/></proof>
@@ -218,7 +218,7 @@
   <proof prover="5"><result status="valid" time="0.017854" steps="104"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.60" expl="precondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.016999" steps="106"/></proof>
+  <proof prover="5"><result status="valid" time="0.016999" steps="105"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.61" expl="precondition" proved="true">
   <proof prover="5"><result status="valid" time="0.017854" steps="80"/></proof>
@@ -227,37 +227,37 @@
   <proof prover="5"><result status="valid" time="0.011820" steps="80"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.63" expl="loop invariant init" proved="true">
-  <proof prover="3"><result status="valid" time="0.010875" steps="13089"/></proof>
+  <proof prover="1"><result status="valid" time="0.010875" steps="13083"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.64" expl="loop invariant init" proved="true">
-  <proof prover="5"><result status="valid" time="0.016613" steps="129"/></proof>
+  <proof prover="5"><result status="valid" time="0.016613" steps="128"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.65" expl="loop invariant init" proved="true">
-  <proof prover="3"><result status="valid" time="0.011486" steps="12949"/></proof>
+  <proof prover="1"><result status="valid" time="0.011486" steps="12943"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.66" expl="loop invariant init" proved="true">
-  <proof prover="5"><result status="valid" time="0.016992" steps="127"/></proof>
+  <proof prover="5"><result status="valid" time="0.016992" steps="126"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.67" expl="loop invariant init" proved="true">
-  <proof prover="5"><result status="valid" time="0.049417" steps="899"/></proof>
+  <proof prover="5"><result status="valid" time="0.049417" steps="879"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.68" expl="loop invariant init" proved="true">
   <proof prover="5"><result status="valid" time="0.018353" steps="150"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.69" expl="loop invariant init" proved="true">
-  <proof prover="5"><result status="valid" time="0.017460" steps="138"/></proof>
+  <proof prover="5"><result status="valid" time="0.017460" steps="137"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.70" expl="precondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.033259" steps="133"/></proof>
+  <proof prover="5"><result status="valid" time="0.033259" steps="132"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.71" expl="type invariant" proved="true">
-  <proof prover="3"><result status="valid" time="0.020043" steps="47152"/></proof>
+  <proof prover="1"><result status="valid" time="0.020043" steps="105900"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.72" expl="loop invariant preservation" proved="true">
-  <proof prover="3"><result status="valid" time="0.040917" steps="176584"/></proof>
+  <proof prover="1"><result status="valid" time="0.040917" steps="196277"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.73" expl="loop invariant preservation" proved="true">
-  <proof prover="5"><result status="valid" time="0.308727" steps="2310"/></proof>
+  <proof prover="5"><result status="valid" time="0.109595" steps="2269"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.74" expl="loop invariant preservation" proved="true">
   <proof prover="5"><result status="valid" time="0.026553" steps="113"/></proof>
@@ -266,52 +266,52 @@
   <proof prover="5"><result status="valid" time="0.049064" steps="149"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.76" expl="loop invariant preservation" proved="true">
-  <proof prover="2"><result status="valid" time="0.380115" steps="60447"/></proof>
+  <proof prover="2"><result status="valid" time="0.380115" steps="60380"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.77" expl="loop invariant preservation" proved="true">
-  <proof prover="3"><result status="valid" time="0.063604" steps="179133"/></proof>
+  <proof prover="1"><result status="valid" time="0.063604" steps="199054"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.78" expl="precondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.163635" steps="1291"/></proof>
+  <proof prover="5"><result status="valid" time="0.163635" steps="1274"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.79" expl="precondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.040623" steps="176"/></proof>
+  <proof prover="5"><result status="valid" time="0.040623" steps="175"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.80" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.072229" steps="174034"/></proof>
+  <proof prover="1"><result status="valid" time="0.072229" steps="194069"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.81" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="1.118080" steps="1421207"/></proof>
+  <proof prover="1"><result status="valid" time="0.136087" steps="732994"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.82" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.037611" steps="13717"/></proof>
+  <proof prover="1"><result status="valid" time="0.037611" steps="13703"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.83" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.037483" steps="174286"/></proof>
+  <proof prover="1"><result status="valid" time="0.037483" steps="194336"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.84" expl="precondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.198534" steps="1291"/></proof>
+  <proof prover="5"><result status="valid" time="0.072129" steps="1278"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.85" expl="precondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.033029" steps="176"/></proof>
+  <proof prover="5"><result status="valid" time="0.033029" steps="175"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.86" expl="precondition" proved="true">
   <proof prover="5"><result status="valid" time="0.015952" steps="176"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.87" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="1.135591" steps="1420732"/></proof>
+  <proof prover="1"><result status="valid" time="0.140035" steps="732689"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.88" expl="precondition" proved="true">
   <proof prover="0"><result status="valid" time="0.107794" steps="22068"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.89" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.035215" steps="174239"/></proof>
+  <proof prover="1"><result status="valid" time="0.035215" steps="194283"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.90" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.041623" steps="206901"/></proof>
+  <proof prover="1"><result status="valid" time="0.041623" steps="207384"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.91" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.033009" steps="174464"/></proof>
+  <proof prover="1"><result status="valid" time="0.033009" steps="194517"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.92" expl="precondition" proved="true">
   <proof prover="5"><result status="valid" time="0.022194" steps="189"/></proof>
@@ -320,66 +320,66 @@
   <proof prover="5"><result status="valid" time="0.022286" steps="255"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.94" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="1.304419" steps="1484516"/></proof>
+  <proof prover="1"><result status="valid" time="0.144794" steps="728019"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.95" expl="precondition" proved="true">
   <proof prover="5"><result status="valid" time="0.015843" steps="136"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.96" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.036658" steps="174863"/></proof>
+  <proof prover="1"><result status="valid" time="0.036658" steps="194954"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.97" expl="integer overflow" proved="true">
-  <proof prover="3"><result status="valid" time="1.094184" steps="1401716"/></proof>
+  <proof prover="1"><result status="valid" time="0.139240" steps="729911"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.98" expl="integer overflow" proved="true">
-  <proof prover="5"><result status="valid" time="0.070200" steps="916"/></proof>
+  <proof prover="5"><result status="valid" time="0.070200" steps="919"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.99" expl="precondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.188844" steps="903"/></proof>
+  <proof prover="5"><result status="valid" time="0.055707" steps="891"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.100" expl="precondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.014599" steps="158"/></proof>
+  <proof prover="5"><result status="valid" time="0.014599" steps="157"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.101" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.032589" steps="183708"/></proof>
+  <proof prover="1"><result status="valid" time="0.032589" steps="204080"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.102" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="1.856247" steps="1913514"/></proof>
+  <proof prover="1"><result status="valid" time="0.136522" steps="747076"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.103" expl="precondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.066507" steps="186"/></proof>
+  <proof prover="5"><result status="valid" time="0.066507" steps="184"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.104" expl="precondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.058942" steps="185"/></proof>
+  <proof prover="5"><result status="valid" time="0.058942" steps="184"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.105" expl="loop invariant preservation" proved="true">
   <proof prover="0"><result status="valid" time="0.128749" steps="26108"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.106" expl="loop invariant preservation" proved="true">
-  <proof prover="3"><result status="valid" time="1.561789" steps="1628660"/></proof>
+  <proof prover="1"><result status="valid" time="0.139440" steps="743051"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.107" expl="loop invariant preservation" proved="true">
-  <proof prover="5"><result status="valid" time="0.014586" steps="216"/></proof>
+  <proof prover="5"><result status="valid" time="0.014586" steps="214"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.108" expl="loop invariant preservation" proved="true">
-  <proof prover="5"><result status="valid" time="0.296517" steps="977"/></proof>
+  <proof prover="5"><result status="valid" time="0.060599" steps="978"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.109" expl="loop invariant preservation" proved="true">
-  <proof prover="5"><result status="valid" time="0.626942" steps="2957"/></proof>
+  <proof prover="5"><result status="valid" time="0.166346" steps="2966"/></proof>
   </goal>
   <goal name="knapsack01_dyn&#39;vc.110" expl="loop invariant preservation" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="knapsack01_dyn&#39;vc.110.0" expl="loop invariant preservation" proved="true">
    <transf name="split_vc" proved="true" >
     <goal name="knapsack01_dyn&#39;vc.110.0.0" expl="loop invariant preservation" proved="true">
-    <proof prover="0"><result status="valid" time="0.931949" steps="97779"/></proof>
+    <proof prover="0"><result status="valid" time="0.676383" steps="97776"/></proof>
     </goal>
     <goal name="knapsack01_dyn&#39;vc.110.0.1" expl="loop invariant preservation" proved="true">
     <transf name="inline_goal" proved="true" >
      <goal name="knapsack01_dyn&#39;vc.110.0.1.0" expl="loop invariant preservation" proved="true">
      <transf name="split_all_full" proved="true" >
       <goal name="knapsack01_dyn&#39;vc.110.0.1.0.0" expl="loop invariant preservation" proved="true">
-      <proof prover="3" timelimit="30" memlimit="4000"><result status="valid" time="2.734949" steps="3565311"/></proof>
+      <proof prover="1" timelimit="30" memlimit="4000"><result status="valid" time="0.123057" steps="725381"/></proof>
       </goal>
      </transf>
      </goal>
diff --git a/creusot/tests/should_succeed/knapsack_full/why3shapes.gz b/creusot/tests/should_succeed/knapsack_full/why3shapes.gz
index 6e5ca9bc4b..a8c285a205 100644
Binary files a/creusot/tests/should_succeed/knapsack_full/why3shapes.gz and b/creusot/tests/should_succeed/knapsack_full/why3shapes.gz differ
diff --git a/creusot/tests/should_succeed/slices/02_std.mlcfg b/creusot/tests/should_succeed/slices/02_std.mlcfg
index 4adf0d409a..45f93c6790 100644
--- a/creusot/tests/should_succeed/slices/02_std.mlcfg
+++ b/creusot/tests/should_succeed/slices/02_std.mlcfg
@@ -601,6 +601,180 @@ module CreusotContracts_Std1_Num_Impl7_DeepModel
   val deep_model (self : uint32) : int
     ensures { result = deep_model self }
     
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Stub
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Interface
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : ()
+  val cmp_le_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_le_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 79 12 79 14] ()
+  val cmp_le_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_le_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Stub
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Interface
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : ()
+  val cmp_lt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_lt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 85 12 85 14] ()
+  val cmp_lt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_lt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Stub
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Interface
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : ()
+  val cmp_ge_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_ge_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 91 12 91 14] ()
+  val cmp_ge_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_ge_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Stub
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Interface
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : ()
+  val cmp_gt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_gt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 97 12 97 14] ()
+  val cmp_gt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_gt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl_Stub
+  use prelude.Int
+  function refl (_1 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl_Interface
+  use prelude.Int
+  function refl (_1 : int) : ()
+  val refl (_1 : int) : ()
+    ensures { result = refl _1 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl
+  use prelude.Int
+  function refl (_1 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 103 12 103 14] ()
+  val refl (_1 : int) : ()
+    ensures { result = refl _1 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans_Stub
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans_Interface
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+  val trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+    ensures { result = trans _1 _2 _3 _4 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 109 12 109 14] ()
+  val trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+    ensures { result = trans _1 _2 _3 _4 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1_Stub
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1_Interface
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : ()
+  val antisym1 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym1 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 115 12 115 14] ()
+  val antisym1 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym1 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2_Stub
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2_Interface
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : ()
+  val antisym2 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym2 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 121 12 121 14] ()
+  val antisym2 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym2 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp_Stub
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp_Interface
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : ()
+  val eq_cmp (_1 : int) (_2 : int) : ()
+    ensures { result = eq_cmp _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 127 12 127 14] ()
+  val eq_cmp (_1 : int) (_2 : int) : ()
+    ensures { result = eq_cmp _1 _2 }
+    
 end
 module CreusotContracts_Logic_Ord_Impl3_LeLog_Stub
   use prelude.Int
@@ -647,6 +821,7 @@ module C02Std_BinarySearch
   use prelude.Slice
   use prelude.UInt32
   use seq.Seq
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
   clone CreusotContracts_Logic_Ord_Impl3_LeLog as LeLog0
   use Core_Result_Result_Type as Core_Result_Result_Type
   clone CreusotContracts_Invariant_Inv_Interface as Inv6 with
@@ -681,6 +856,15 @@ module C02Std_BinarySearch
     type t = slice uint32,
     predicate Inv0.inv = Inv2.inv,
     axiom .
+  clone CreusotContracts_Logic_Ord_Impl3_EqCmp_Interface as EqCmp0
+  clone CreusotContracts_Logic_Ord_Impl3_Antisym2_Interface as Antisym20
+  clone CreusotContracts_Logic_Ord_Impl3_Antisym1_Interface as Antisym10
+  clone CreusotContracts_Logic_Ord_Impl3_Trans_Interface as Trans0
+  clone CreusotContracts_Logic_Ord_Impl3_Refl_Interface as Refl0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Interface as CmpGtLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Interface as CmpGeLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Interface as CmpLtLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Interface as CmpLeLog0
   clone CreusotContracts_Invariant_Inv_Interface as Inv1 with
     type t = uint32
   clone TyInv_Trivial as TyInv_Trivial1 with
diff --git a/creusot/tests/should_succeed/slices/02_std/why3session.xml b/creusot/tests/should_succeed/slices/02_std/why3session.xml
index 1a7fc0df4b..e597d67f83 100644
--- a/creusot/tests/should_succeed/slices/02_std/why3session.xml
+++ b/creusot/tests/should_succeed/slices/02_std/why3session.xml
@@ -9,29 +9,29 @@
  <goal name="binary_search&#39;vc" expl="VC for binary_search" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="binary_search&#39;vc.0" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.010000" steps="82"/></proof>
+  <proof prover="0"><result status="valid" time="0.010000" steps="79"/></proof>
   </goal>
   <goal name="binary_search&#39;vc.1" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.017370" steps="20"/></proof>
+  <proof prover="0"><result status="valid" time="0.017370" steps="19"/></proof>
   </goal>
   <goal name="binary_search&#39;vc.2" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.013155" steps="21"/></proof>
+  <proof prover="0"><result status="valid" time="0.013155" steps="20"/></proof>
   </goal>
   <goal name="binary_search&#39;vc.3" expl="precondition" proved="true">
   <transf name="destruct_term" proved="true" arg1="_5">
    <goal name="binary_search&#39;vc.3.0" expl="precondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.126562" steps="985"/></proof>
+   <proof prover="0"><result status="valid" time="0.126562" steps="982"/></proof>
    </goal>
    <goal name="binary_search&#39;vc.3.1" expl="precondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.020800" steps="45"/></proof>
+   <proof prover="0"><result status="valid" time="0.020800" steps="44"/></proof>
    </goal>
   </transf>
   </goal>
   <goal name="binary_search&#39;vc.4" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.022953" steps="26"/></proof>
+  <proof prover="0"><result status="valid" time="0.022953" steps="25"/></proof>
   </goal>
   <goal name="binary_search&#39;vc.5" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="0.010000" steps="27"/></proof>
+  <proof prover="0"><result status="valid" time="0.010000" steps="26"/></proof>
   </goal>
  </transf>
  </goal>
diff --git a/creusot/tests/should_succeed/slices/02_std/why3shapes.gz b/creusot/tests/should_succeed/slices/02_std/why3shapes.gz
index 656388df88..3da06821c0 100644
Binary files a/creusot/tests/should_succeed/slices/02_std/why3shapes.gz and b/creusot/tests/should_succeed/slices/02_std/why3shapes.gz differ
diff --git a/creusot/tests/should_succeed/sum.mlcfg b/creusot/tests/should_succeed/sum.mlcfg
index 9fb8863acc..3d363ceaec 100644
--- a/creusot/tests/should_succeed/sum.mlcfg
+++ b/creusot/tests/should_succeed/sum.mlcfg
@@ -815,6 +815,180 @@ module CreusotContracts_Std1_Iter_Range_Impl1_Completed
   val completed (self : borrowed (Core_Ops_Range_RangeInclusive_Type.t_rangeinclusive idx)) : bool
     ensures { result = completed self }
     
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Stub
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Interface
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : ()
+  val cmp_le_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_le_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 79 12 79 14] ()
+  val cmp_le_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_le_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Stub
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Interface
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : ()
+  val cmp_lt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_lt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 85 12 85 14] ()
+  val cmp_lt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_lt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Stub
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Interface
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : ()
+  val cmp_ge_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_ge_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 91 12 91 14] ()
+  val cmp_ge_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_ge_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Stub
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Interface
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : ()
+  val cmp_gt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_gt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 97 12 97 14] ()
+  val cmp_gt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_gt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl_Stub
+  use prelude.Int
+  function refl (_1 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl_Interface
+  use prelude.Int
+  function refl (_1 : int) : ()
+  val refl (_1 : int) : ()
+    ensures { result = refl _1 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl
+  use prelude.Int
+  function refl (_1 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 103 12 103 14] ()
+  val refl (_1 : int) : ()
+    ensures { result = refl _1 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans_Stub
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans_Interface
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+  val trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+    ensures { result = trans _1 _2 _3 _4 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 109 12 109 14] ()
+  val trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+    ensures { result = trans _1 _2 _3 _4 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1_Stub
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1_Interface
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : ()
+  val antisym1 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym1 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 115 12 115 14] ()
+  val antisym1 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym1 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2_Stub
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2_Interface
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : ()
+  val antisym2 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym2 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 121 12 121 14] ()
+  val antisym2 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym2 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp_Stub
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp_Interface
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : ()
+  val eq_cmp (_1 : int) (_2 : int) : ()
+    ensures { result = eq_cmp _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : () =
+    [#"../../../../creusot-contracts/src/logic/ord.rs" 127 12 127 14] ()
+  val eq_cmp (_1 : int) (_2 : int) : ()
+    ensures { result = eq_cmp _1 _2 }
+    
 end
 module Sum_SumFirstN_Interface
   use prelude.UInt32
@@ -837,6 +1011,7 @@ module Sum_SumFirstN
     type t = Seq.seq uint32,
     predicate Inv0.inv = Inv4.inv,
     axiom .
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
   use Core_Option_Option_Type as Core_Option_Option_Type
   clone CreusotContracts_Invariant_Inv_Interface as Inv3 with
     type t = Core_Option_Option_Type.t_option uint32
@@ -851,6 +1026,15 @@ module Sum_SumFirstN
     type t = borrowed (Core_Ops_Range_RangeInclusive_Type.t_rangeinclusive uint32),
     predicate Inv0.inv = Inv2.inv,
     axiom .
+  clone CreusotContracts_Logic_Ord_Impl3_EqCmp_Interface as EqCmp0
+  clone CreusotContracts_Logic_Ord_Impl3_Antisym2_Interface as Antisym20
+  clone CreusotContracts_Logic_Ord_Impl3_Antisym1_Interface as Antisym10
+  clone CreusotContracts_Logic_Ord_Impl3_Trans_Interface as Trans0
+  clone CreusotContracts_Logic_Ord_Impl3_Refl_Interface as Refl0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Interface as CmpGtLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Interface as CmpGeLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Interface as CmpLtLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Interface as CmpLeLog0
   clone CreusotContracts_Invariant_Inv_Interface as Inv1 with
     type t = uint32
   clone TyInv_Trivial as TyInv_Trivial1 with
diff --git a/creusot/tests/should_succeed/sum/why3session.xml b/creusot/tests/should_succeed/sum/why3session.xml
index 6125693839..bfa8cce7cc 100644
--- a/creusot/tests/should_succeed/sum/why3session.xml
+++ b/creusot/tests/should_succeed/sum/why3session.xml
@@ -4,14 +4,14 @@
 <why3session shape_version="6">
 <prover id="0" name="Alt-Ergo" version="2.4.2" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="CVC5" version="1.0.5" timelimit="1" steplimit="0" memlimit="1000"/>
-<prover id="3" name="Z3" version="4.12.1" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="2" name="Z3" version="4.11.2" timelimit="1" steplimit="0" memlimit="1000"/>
 <file format="mlcfg" proved="true">
 <path name=".."/><path name="sum.mlcfg"/>
 <theory name="Sum_SumFirstN" proved="true">
  <goal name="sum_first_n&#39;vc" expl="VC for sum_first_n" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="sum_first_n&#39;vc.0" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.013914" steps="41513"/></proof>
+  <proof prover="2"><result status="valid" time="0.013914" steps="46455"/></proof>
   </goal>
   <goal name="sum_first_n&#39;vc.1" expl="precondition" proved="true">
   <proof prover="0"><result status="valid" time="0.106520" steps="19"/></proof>
@@ -23,7 +23,7 @@
   <proof prover="0"><result status="valid" time="0.008401" steps="16"/></proof>
   </goal>
   <goal name="sum_first_n&#39;vc.4" expl="loop invariant init" proved="true">
-  <proof prover="3"><result status="valid" time="0.008354" steps="3858"/></proof>
+  <proof prover="2"><result status="valid" time="0.008354" steps="3858"/></proof>
   </goal>
   <goal name="sum_first_n&#39;vc.5" expl="loop invariant init" proved="true">
   <proof prover="0"><result status="valid" time="0.008896" steps="37"/></proof>
@@ -32,10 +32,10 @@
   <proof prover="0"><result status="valid" time="0.014020" steps="215"/></proof>
   </goal>
   <goal name="sum_first_n&#39;vc.7" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.007377" steps="102"/></proof>
+  <proof prover="0"><result status="valid" time="0.007377" steps="101"/></proof>
   </goal>
   <goal name="sum_first_n&#39;vc.8" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="1.297002" steps="14357"/></proof>
+  <proof prover="0"><result status="valid" time="0.405841" steps="14361"/></proof>
   </goal>
   <goal name="sum_first_n&#39;vc.9" expl="integer overflow" proved="true">
   <transf name="split_vc" proved="true" >
@@ -49,7 +49,7 @@
      <goal name="sum_first_n&#39;vc.9.0.0.1" expl="VC for sum_first_n" proved="true">
      <transf name="inline_goal" proved="true" >
       <goal name="sum_first_n&#39;vc.9.0.0.1.0" expl="VC for sum_first_n" proved="true">
-      <proof prover="3" timelimit="30" memlimit="4000"><result status="valid" time="2.985778" steps="2745056"/></proof>
+      <proof prover="2" timelimit="30" memlimit="4000"><result status="valid" time="0.251319" steps="1076869"/></proof>
       </goal>
      </transf>
      </goal>
@@ -63,15 +63,15 @@
   <proof prover="1"><result status="valid" time="0.108026" steps="11558"/></proof>
   </goal>
   <goal name="sum_first_n&#39;vc.11" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="0.526379" steps="4693"/></proof>
+  <proof prover="0"><result status="valid" time="0.173264" steps="4705"/></proof>
   </goal>
   <goal name="sum_first_n&#39;vc.12" expl="loop invariant preservation" proved="true">
   <transf name="assert" proved="true" arg1="(to_int i = length (inner produced))">
    <goal name="sum_first_n&#39;vc.12.0" expl="asserted formula" proved="true">
-   <proof prover="0"><result status="valid" time="0.100016" steps="1242"/></proof>
+   <proof prover="0"><result status="valid" time="0.100016" steps="1240"/></proof>
    </goal>
    <goal name="sum_first_n&#39;vc.12.1" expl="loop invariant preservation" proved="true">
-   <proof prover="0"><result status="valid" time="0.581701" steps="3556"/></proof>
+   <proof prover="0"><result status="valid" time="0.235500" steps="3565"/></proof>
    </goal>
   </transf>
   </goal>
diff --git a/creusot/tests/should_succeed/sum/why3shapes.gz b/creusot/tests/should_succeed/sum/why3shapes.gz
index 0b3ab7909d..345b44b369 100644
Binary files a/creusot/tests/should_succeed/sum/why3shapes.gz and b/creusot/tests/should_succeed/sum/why3shapes.gz differ
diff --git a/creusot/tests/should_succeed/syntax/10_mutual_rec_types.mlcfg b/creusot/tests/should_succeed/syntax/10_mutual_rec_types.mlcfg
index 734d62794d..152fbf45d5 100644
--- a/creusot/tests/should_succeed/syntax/10_mutual_rec_types.mlcfg
+++ b/creusot/tests/should_succeed/syntax/10_mutual_rec_types.mlcfg
@@ -310,6 +310,180 @@ module CreusotContracts_Logic_Ord_Impl3_LtLog
   val lt_log (self : int) (_2 : int) : bool
     ensures { result = lt_log self _2 }
     
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Stub
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Interface
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : ()
+  val cmp_le_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_le_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 79 12 79 14] ()
+  val cmp_le_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_le_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Stub
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Interface
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : ()
+  val cmp_lt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_lt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 85 12 85 14] ()
+  val cmp_lt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_lt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Stub
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Interface
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : ()
+  val cmp_ge_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_ge_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 91 12 91 14] ()
+  val cmp_ge_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_ge_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Stub
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Interface
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : ()
+  val cmp_gt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_gt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 97 12 97 14] ()
+  val cmp_gt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_gt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl_Stub
+  use prelude.Int
+  function refl (_1 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl_Interface
+  use prelude.Int
+  function refl (_1 : int) : ()
+  val refl (_1 : int) : ()
+    ensures { result = refl _1 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl
+  use prelude.Int
+  function refl (_1 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 103 12 103 14] ()
+  val refl (_1 : int) : ()
+    ensures { result = refl _1 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans_Stub
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans_Interface
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+  val trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+    ensures { result = trans _1 _2 _3 _4 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 109 12 109 14] ()
+  val trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+    ensures { result = trans _1 _2 _3 _4 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1_Stub
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1_Interface
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : ()
+  val antisym1 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym1 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 115 12 115 14] ()
+  val antisym1 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym1 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2_Stub
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2_Interface
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : ()
+  val antisym2 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym2 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 121 12 121 14] ()
+  val antisym2 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym2 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp_Stub
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp_Interface
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : ()
+  val eq_cmp (_1 : int) (_2 : int) : ()
+    ensures { result = eq_cmp _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 127 12 127 14] ()
+  val eq_cmp (_1 : int) (_2 : int) : ()
+    ensures { result = eq_cmp _1 _2 }
+    
 end
 module C10MutualRecTypes_Impl0_Height_Interface
   use prelude.Borrow
@@ -322,6 +496,16 @@ module C10MutualRecTypes_Impl0_Height
   use prelude.Int
   use prelude.UInt64
   use prelude.Borrow
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  clone CreusotContracts_Logic_Ord_Impl3_EqCmp_Interface as EqCmp0
+  clone CreusotContracts_Logic_Ord_Impl3_Antisym2_Interface as Antisym20
+  clone CreusotContracts_Logic_Ord_Impl3_Antisym1_Interface as Antisym10
+  clone CreusotContracts_Logic_Ord_Impl3_Trans_Interface as Trans0
+  clone CreusotContracts_Logic_Ord_Impl3_Refl_Interface as Refl0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Interface as CmpGtLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Interface as CmpGeLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Interface as CmpLtLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Interface as CmpLeLog0
   clone CreusotContracts_Invariant_Inv_Interface as Inv0 with
     type t = uint64
   clone TyInv_Trivial as TyInv_Trivial0 with
diff --git a/creusot/tests/should_succeed/vector/08_haystack.mlcfg b/creusot/tests/should_succeed/vector/08_haystack.mlcfg
index 58f8f2b5af..8a016502aa 100644
--- a/creusot/tests/should_succeed/vector/08_haystack.mlcfg
+++ b/creusot/tests/should_succeed/vector/08_haystack.mlcfg
@@ -1465,6 +1465,180 @@ module CreusotContracts_Std1_Slice_Impl5_HasValue
   val has_value [@inline:trivial] (self : usize) (seq : Seq.seq t) (out : t) : bool
     ensures { result = has_value self seq out }
     
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Stub
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Interface
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : ()
+  val cmp_le_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_le_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLeLog
+  use prelude.Int
+  function cmp_le_log (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 79 12 79 14] ()
+  val cmp_le_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_le_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Stub
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Interface
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : ()
+  val cmp_lt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_lt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpLtLog
+  use prelude.Int
+  function cmp_lt_log (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 85 12 85 14] ()
+  val cmp_lt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_lt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Stub
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Interface
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : ()
+  val cmp_ge_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_ge_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGeLog
+  use prelude.Int
+  function cmp_ge_log (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 91 12 91 14] ()
+  val cmp_ge_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_ge_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Stub
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Interface
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : ()
+  val cmp_gt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_gt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_CmpGtLog
+  use prelude.Int
+  function cmp_gt_log (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 97 12 97 14] ()
+  val cmp_gt_log (_1 : int) (_2 : int) : ()
+    ensures { result = cmp_gt_log _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl_Stub
+  use prelude.Int
+  function refl (_1 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl_Interface
+  use prelude.Int
+  function refl (_1 : int) : ()
+  val refl (_1 : int) : ()
+    ensures { result = refl _1 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Refl
+  use prelude.Int
+  function refl (_1 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 103 12 103 14] ()
+  val refl (_1 : int) : ()
+    ensures { result = refl _1 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans_Stub
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans_Interface
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+  val trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+    ensures { result = trans _1 _2 _3 _4 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Trans
+  use prelude.Int
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
+  function trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 109 12 109 14] ()
+  val trans (_1 : int) (_2 : int) (_3 : int) (_4 : Core_Cmp_Ordering_Type.t_ordering) : ()
+    ensures { result = trans _1 _2 _3 _4 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1_Stub
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1_Interface
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : ()
+  val antisym1 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym1 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym1
+  use prelude.Int
+  function antisym1 (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 115 12 115 14] ()
+  val antisym1 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym1 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2_Stub
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2_Interface
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : ()
+  val antisym2 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym2 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_Antisym2
+  use prelude.Int
+  function antisym2 (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 121 12 121 14] ()
+  val antisym2 (_1 : int) (_2 : int) : ()
+    ensures { result = antisym2 _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp_Stub
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : ()
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp_Interface
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : ()
+  val eq_cmp (_1 : int) (_2 : int) : ()
+    ensures { result = eq_cmp _1 _2 }
+    
+end
+module CreusotContracts_Logic_Ord_Impl3_EqCmp
+  use prelude.Int
+  function eq_cmp (_1 : int) (_2 : int) : () =
+    [#"../../../../../creusot-contracts/src/logic/ord.rs" 127 12 127 14] ()
+  val eq_cmp (_1 : int) (_2 : int) : ()
+    ensures { result = eq_cmp _1 _2 }
+    
 end
 module C08Haystack_Search_Interface
   use seq.Seq
@@ -1514,6 +1688,7 @@ module C08Haystack_Search
     type t = Seq.seq usize,
     predicate Inv0.inv = Inv8.inv,
     axiom .
+  use Core_Cmp_Ordering_Type as Core_Cmp_Ordering_Type
   clone CreusotContracts_Invariant_Inv_Interface as Inv7 with
     type t = uint8
   clone TyInv_Trivial as TyInv_Trivial7 with
@@ -1542,6 +1717,15 @@ module C08Haystack_Search
     predicate Inv0.inv = Inv4.inv,
     axiom .
   clone Core_Num_Impl11_Max as Max0
+  clone CreusotContracts_Logic_Ord_Impl3_EqCmp_Interface as EqCmp0
+  clone CreusotContracts_Logic_Ord_Impl3_Antisym2_Interface as Antisym20
+  clone CreusotContracts_Logic_Ord_Impl3_Antisym1_Interface as Antisym10
+  clone CreusotContracts_Logic_Ord_Impl3_Trans_Interface as Trans0
+  clone CreusotContracts_Logic_Ord_Impl3_Refl_Interface as Refl0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpGtLog_Interface as CmpGtLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpGeLog_Interface as CmpGeLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpLtLog_Interface as CmpLtLog0
+  clone CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Interface as CmpLeLog0
   clone CreusotContracts_Invariant_Inv_Interface as Inv3 with
     type t = usize
   clone TyInv_Trivial as TyInv_Trivial3 with
diff --git a/creusot/tests/should_succeed/vector/08_haystack/why3session.xml b/creusot/tests/should_succeed/vector/08_haystack/why3session.xml
index 9538239768..90a474bd5c 100644
--- a/creusot/tests/should_succeed/vector/08_haystack/why3session.xml
+++ b/creusot/tests/should_succeed/vector/08_haystack/why3session.xml
@@ -2,7 +2,7 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="6">
-<prover id="1" name="Z3" version="4.12.1" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="0" name="Z3" version="4.11.2" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Alt-Ergo" version="2.4.2" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="3" name="CVC5" version="1.0.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <file format="mlcfg" proved="true">
@@ -14,31 +14,31 @@
   <proof prover="3"><result status="valid" time="0.155020" steps="11262"/></proof>
   </goal>
   <goal name="search&#39;vc.1" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.028733" steps="78009"/></proof>
+  <proof prover="0"><result status="valid" time="0.028733" steps="84507"/></proof>
   </goal>
   <goal name="search&#39;vc.2" expl="integer overflow" proved="true">
-  <proof prover="2"><result status="valid" time="0.009606" steps="24"/></proof>
+  <proof prover="2"><result status="valid" time="0.009606" steps="23"/></proof>
   </goal>
   <goal name="search&#39;vc.3" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.016841" steps="30"/></proof>
+  <proof prover="2"><result status="valid" time="0.016841" steps="29"/></proof>
   </goal>
   <goal name="search&#39;vc.4" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.019284" steps="78646"/></proof>
+  <proof prover="0"><result status="valid" time="0.019284" steps="85188"/></proof>
   </goal>
   <goal name="search&#39;vc.5" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.008654" steps="19"/></proof>
+  <proof prover="2"><result status="valid" time="0.008654" steps="18"/></proof>
   </goal>
   <goal name="search&#39;vc.6" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.035544" steps="6802"/></proof>
+  <proof prover="0"><result status="valid" time="0.035544" steps="6802"/></proof>
   </goal>
   <goal name="search&#39;vc.7" expl="loop invariant init" proved="true">
   <proof prover="2"><result status="valid" time="0.010443" steps="25"/></proof>
   </goal>
   <goal name="search&#39;vc.8" expl="loop invariant init" proved="true">
-  <proof prover="2"><result status="valid" time="0.010430" steps="48"/></proof>
+  <proof prover="2"><result status="valid" time="0.010430" steps="47"/></proof>
   </goal>
   <goal name="search&#39;vc.9" expl="loop invariant init" proved="true">
-  <proof prover="1"><result status="valid" time="0.023052" steps="111688"/></proof>
+  <proof prover="0"><result status="valid" time="0.023052" steps="124542"/></proof>
   </goal>
   <goal name="search&#39;vc.10" expl="precondition" proved="true">
   <proof prover="2"><result status="valid" time="0.030444" steps="52"/></proof>
@@ -47,13 +47,13 @@
   <proof prover="2"><result status="valid" time="0.008926" steps="56"/></proof>
   </goal>
   <goal name="search&#39;vc.12" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.019476" steps="117187"/></proof>
+  <proof prover="0"><result status="valid" time="0.019476" steps="130704"/></proof>
   </goal>
   <goal name="search&#39;vc.13" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.009955" steps="9225"/></proof>
+  <proof prover="0"><result status="valid" time="0.009955" steps="9225"/></proof>
   </goal>
   <goal name="search&#39;vc.14" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.086810" steps="81"/></proof>
+  <proof prover="2"><result status="valid" time="0.086810" steps="79"/></proof>
   </goal>
   <goal name="search&#39;vc.15" expl="loop invariant init" proved="true">
   <proof prover="2"><result status="valid" time="0.008849" steps="65"/></proof>
@@ -62,25 +62,25 @@
   <proof prover="2"><result status="valid" time="0.013109" steps="94"/></proof>
   </goal>
   <goal name="search&#39;vc.17" expl="loop invariant init" proved="true">
-  <proof prover="1"><result status="valid" time="0.354446" steps="559499"/></proof>
+  <proof prover="0"><result status="valid" time="0.075230" steps="412578"/></proof>
   </goal>
   <goal name="search&#39;vc.18" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.024488" steps="120265"/></proof>
+  <proof prover="0"><result status="valid" time="0.024488" steps="134017"/></proof>
   </goal>
   <goal name="search&#39;vc.19" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.209528" steps="963"/></proof>
+  <proof prover="2"><result status="valid" time="0.055409" steps="967"/></proof>
   </goal>
   <goal name="search&#39;vc.20" expl="precondition" proved="true">
   <proof prover="2"><result status="valid" time="0.020785" steps="131"/></proof>
   </goal>
   <goal name="search&#39;vc.21" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.018639" steps="133"/></proof>
+  <proof prover="2"><result status="valid" time="0.018639" steps="131"/></proof>
   </goal>
   <goal name="search&#39;vc.22" expl="integer overflow" proved="true">
-  <proof prover="1"><result status="valid" time="0.027655" steps="158666"/></proof>
+  <proof prover="0"><result status="valid" time="0.027655" steps="152896"/></proof>
   </goal>
   <goal name="search&#39;vc.23" expl="precondition" proved="true">
-  <proof prover="1"><result status="valid" time="1.075828" steps="1174393"/></proof>
+  <proof prover="0"><result status="valid" time="0.114528" steps="620054"/></proof>
   </goal>
   <goal name="search&#39;vc.24" expl="precondition" proved="true">
   <proof prover="2"><result status="valid" time="0.009833" steps="142"/></proof>
@@ -92,28 +92,28 @@
   <proof prover="3"><result status="valid" time="0.191848" steps="18051"/></proof>
   </goal>
   <goal name="search&#39;vc.27" expl="loop invariant preservation" proved="true">
-  <proof prover="1"><result status="valid" time="1.096586" steps="1383344"/></proof>
+  <proof prover="0"><result status="valid" time="0.119033" steps="624778"/></proof>
   </goal>
   <goal name="search&#39;vc.28" expl="loop invariant preservation" proved="true">
-  <proof prover="3"><result status="valid" time="0.652882" steps="50295"/></proof>
+  <proof prover="3"><result status="valid" time="0.326537" steps="50293"/></proof>
   </goal>
   <goal name="search&#39;vc.29" expl="loop invariant preservation" proved="true">
-  <proof prover="1"><result status="valid" time="0.029358" steps="131941"/></proof>
+  <proof prover="0"><result status="valid" time="0.029358" steps="146430"/></proof>
   </goal>
   <goal name="search&#39;vc.30" expl="loop invariant preservation" proved="true">
-  <proof prover="2"><result status="valid" time="0.704137" steps="2678"/></proof>
+  <proof prover="2"><result status="valid" time="0.151645" steps="2638"/></proof>
   </goal>
   <goal name="search&#39;vc.31" expl="loop invariant preservation" proved="true">
-  <proof prover="2"><result status="valid" time="1.259282" steps="7835"/></proof>
+  <proof prover="2"><result status="valid" time="0.329596" steps="7202"/></proof>
   </goal>
   <goal name="search&#39;vc.32" expl="postcondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.296736" steps="22306"/></proof>
+  <proof prover="3"><result status="valid" time="0.139861" steps="22306"/></proof>
   </goal>
   <goal name="search&#39;vc.33" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.524357" steps="621383"/></proof>
+  <proof prover="0"><result status="valid" time="0.083467" steps="447276"/></proof>
   </goal>
   <goal name="search&#39;vc.34" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.182961" steps="274286"/></proof>
+  <proof prover="0"><result status="valid" time="0.046369" steps="285721"/></proof>
   </goal>
  </transf>
  </goal>
diff --git a/creusot/tests/should_succeed/vector/08_haystack/why3shapes.gz b/creusot/tests/should_succeed/vector/08_haystack/why3shapes.gz
index d154386231..68991feb11 100644
Binary files a/creusot/tests/should_succeed/vector/08_haystack/why3shapes.gz and b/creusot/tests/should_succeed/vector/08_haystack/why3shapes.gz differ
diff --git a/why3/src/declaration.rs b/why3/src/declaration.rs
index c3a491713d..ae0d3fa566 100644
--- a/why3/src/declaration.rs
+++ b/why3/src/declaration.rs
@@ -2,7 +2,7 @@ use indexmap::IndexSet;
 use std::collections::{BTreeMap, HashMap};
 
 use crate::{
-    exp::{Binder, Exp, ExpMutVisitor},
+    exp::{Binder, Exp, ExpMutVisitor, Trigger},
     mlcfg::{Block, BlockId},
     ty::Type,
     *,
@@ -143,6 +143,7 @@ pub enum Attribute {
 #[cfg_attr(feature = "serialize", derive(Serialize, Deserialize))]
 pub struct Signature {
     pub name: Ident,
+    pub trigger: Option<Trigger>, // None means Trigger::single(function_call(self))
     pub attrs: Vec<Attribute>,
     pub retty: Option<Type>,
     pub args: Vec<Binder>,
diff --git a/why3/src/exp.rs b/why3/src/exp.rs
index d08375d0b0..772621ed94 100644
--- a/why3/src/exp.rs
+++ b/why3/src/exp.rs
@@ -94,6 +94,19 @@ pub enum Purity {
     Program,
 }
 
+#[derive(Debug, Clone)]
+#[cfg_attr(feature = "serialize", derive(Serialize, Deserialize))]
+// TODO: multi-trigger/multiple triggers
+pub struct Trigger(pub Option<Box<Exp>>);
+
+impl Trigger {
+    pub const NONE: Trigger = Trigger(None);
+
+    pub fn single(exp: Exp) -> Self {
+        Trigger(Some(Box::new(exp)))
+    }
+}
+
 // TODO: Should we introduce an 'ExprKind' struct which wraps `Exp` with attributes?
 #[derive(Debug, Clone)]
 #[cfg_attr(feature = "serialize", derive(Serialize, Deserialize))]
@@ -128,8 +141,8 @@ pub enum Exp {
     Old(Box<Exp>),
     Absurd,
     Impl(Box<Exp>, Box<Exp>),
-    Forall(Vec<(Ident, Type)>, Box<Exp>),
-    Exists(Vec<(Ident, Type)>, Box<Exp>),
+    Forall(Vec<(Ident, Type)>, Trigger, Box<Exp>),
+    Exists(Vec<(Ident, Type)>, Trigger, Box<Exp>),
     Sequence(Vec<Exp>),
     FnLit(Box<Exp>),
 }
@@ -147,6 +160,10 @@ pub trait ExpMutVisitor: Sized {
     fn visit_mut(&mut self, exp: &mut Exp) {
         super_visit_mut(self, exp)
     }
+
+    fn visit_trigger_mut(&mut self, trig: &mut Trigger) {
+        super_visit_mut_trigger(self, trig)
+    }
 }
 
 pub fn super_visit_mut<T: ExpMutVisitor>(f: &mut T, exp: &mut Exp) {
@@ -196,8 +213,14 @@ pub fn super_visit_mut<T: ExpMutVisitor>(f: &mut T, exp: &mut Exp) {
             f.visit_mut(l);
             f.visit_mut(r)
         }
-        Exp::Forall(_, e) => f.visit_mut(e),
-        Exp::Exists(_, e) => f.visit_mut(e),
+        Exp::Forall(_, t, e) => {
+            f.visit_trigger_mut(t);
+            f.visit_mut(e)
+        }
+        Exp::Exists(_, t, e) => {
+            f.visit_trigger_mut(t);
+            f.visit_mut(e)
+        }
         Exp::Attr(_, e) => f.visit_mut(e),
         Exp::Ghost(e) => f.visit_mut(e),
         Exp::Record { fields } => fields.iter_mut().for_each(|(_, e)| f.visit_mut(e)),
@@ -207,10 +230,21 @@ pub fn super_visit_mut<T: ExpMutVisitor>(f: &mut T, exp: &mut Exp) {
     }
 }
 
+pub fn super_visit_mut_trigger<T: ExpMutVisitor>(f: &mut T, trigger: &mut Trigger) {
+    match &mut trigger.0 {
+        None => {}
+        Some(exp) => f.visit_mut(exp),
+    }
+}
+
 pub trait ExpVisitor: Sized {
     fn visit(&mut self, exp: &Exp) {
         super_visit(self, exp)
     }
+
+    fn visit_trigger(&mut self, trig: &Trigger) {
+        super_visit_trigger(self, trig)
+    }
 }
 
 pub fn super_visit<T: ExpVisitor>(f: &mut T, exp: &Exp) {
@@ -260,8 +294,14 @@ pub fn super_visit<T: ExpVisitor>(f: &mut T, exp: &Exp) {
             f.visit(l);
             f.visit(r)
         }
-        Exp::Forall(_, e) => f.visit(e),
-        Exp::Exists(_, e) => f.visit(e),
+        Exp::Forall(_, t, e) => {
+            f.visit_trigger(t);
+            f.visit(e)
+        }
+        Exp::Exists(_, t, e) => {
+            f.visit_trigger(t);
+            f.visit(e)
+        }
         Exp::Attr(_, e) => f.visit(e),
         Exp::Ghost(e) => f.visit(e),
         Exp::Record { fields } => fields.iter().for_each(|(_, e)| f.visit(e)),
@@ -271,6 +311,13 @@ pub fn super_visit<T: ExpVisitor>(f: &mut T, exp: &Exp) {
     }
 }
 
+pub fn super_visit_trigger<T: ExpVisitor>(f: &mut T, trigger: &Trigger) {
+    match &trigger.0 {
+        None => {}
+        Some(exp) => f.visit(exp),
+    }
+}
+
 impl Exp {
     pub fn impure_qvar(q: QName) -> Self {
         Exp::QVar(q, Purity::Program)
@@ -355,6 +402,22 @@ impl Exp {
         }
     }
 
+    pub fn forall_trig(bound: Vec<(Ident, Type)>, trigger: Trigger, body: Exp) -> Self {
+        Exp::Forall(bound, trigger, Box::new(body))
+    }
+
+    pub fn forall(bound: Vec<(Ident, Type)>, body: Exp) -> Self {
+        Exp::forall_trig(bound, Trigger::NONE, body)
+    }
+
+    pub fn exists_trig(bound: Vec<(Ident, Type)>, trigger: Trigger, body: Exp) -> Self {
+        Exp::Exists(bound, trigger, Box::new(body))
+    }
+
+    pub fn exists(bound: Vec<(Ident, Type)>, body: Exp) -> Self {
+        Exp::exists_trig(bound, Trigger::NONE, body)
+    }
+
     pub fn is_true(&self) -> bool {
         if let Exp::Const(Constant::Bool(true)) = self {
             true
@@ -551,8 +614,8 @@ impl Exp {
             Exp::Call(_, _) => App,
             // Exp::Verbatim(_) => Any,
             Exp::Impl(_, _) => Impl,
-            Exp::Forall(_, _) => IfLet,
-            Exp::Exists(_, _) => IfLet,
+            Exp::Forall(_, _, _) => IfLet,
+            Exp::Exists(_, _, _) => IfLet,
             Exp::Ascribe(_, _) => Cast,
             Exp::Absurd => Atom,
             Exp::Pure(_) => Atom,
@@ -587,19 +650,19 @@ impl Exp {
                         self.visit(arg);
                         self.fvs.extend(fvs);
                     }
-                    Exp::Forall(bnds, exp) => {
+                    Exp::Forall(bnds, trig, exp) => {
                         let fvs = std::mem::take(&mut self.fvs);
                         self.visit(exp);
-
+                        self.visit_trigger(trig);
                         bnds.iter().for_each(|(l, _)| {
                             self.fvs.remove(l);
                         });
                         self.fvs.extend(fvs);
                     }
-                    Exp::Exists(bnds, exp) => {
+                    Exp::Exists(bnds, trig, exp) => {
                         let fvs = std::mem::take(&mut self.fvs);
                         self.visit(exp);
-
+                        self.visit_trigger(trig);
                         bnds.iter().for_each(|(l, _)| {
                             self.fvs.remove(l);
                         });
@@ -684,21 +747,23 @@ impl Exp {
                             s.visit_mut(br);
                         }
                     }
-                    Exp::Forall(binders, exp) => {
+                    Exp::Forall(binders, trig, exp) => {
                         let mut subst = self.clone();
                         binders.iter().for_each(|k| {
                             subst.remove(&k.0);
                         });
                         let mut s = &subst;
                         s.visit_mut(exp);
+                        s.visit_trigger_mut(trig);
                     }
-                    Exp::Exists(binders, exp) => {
+                    Exp::Exists(binders, trig, exp) => {
                         let mut subst = self.clone();
                         binders.iter().for_each(|k| {
                             subst.remove(&k.0);
                         });
                         let mut s = &subst;
                         s.visit_mut(exp);
+                        s.visit_trigger_mut(trig);
                     }
                     _ => super_visit_mut(self, exp),
                 }
diff --git a/why3/src/mlcfg/printer.rs b/why3/src/mlcfg/printer.rs
index 8a2f662c87..64c0a4bb8f 100644
--- a/why3/src/mlcfg/printer.rs
+++ b/why3/src/mlcfg/printer.rs
@@ -3,7 +3,7 @@ use std::{fmt::Display, iter::once};
 use super::*;
 use crate::{
     declaration::*,
-    exp::{AssocDir, BinOp, Binder, Constant, Precedence, UnOp},
+    exp::{AssocDir, BinOp, Binder, Constant, Precedence, Trigger, UnOp},
 };
 use num::{Float, Zero};
 use pretty::*;
@@ -614,6 +614,22 @@ impl Print for Type {
     }
 }
 
+impl Print for Trigger {
+    fn pretty<'b, 'a: 'b, A: DocAllocator<'a>>(
+        &'a self,
+        alloc: &'a A,
+        env: &mut PrintEnv,
+    ) -> DocBuilder<'a, A>
+    where
+        A::Doc: Clone,
+    {
+        match &self.0 {
+            None => alloc.nil(),
+            Some(exp) => exp.pretty(alloc, env).brackets(),
+        }
+    }
+}
+
 impl Print for Exp {
     fn pretty<'b, 'a: 'b, A: DocAllocator<'a>>(
         &'a self,
@@ -730,7 +746,7 @@ impl Print for Exp {
                 .append("else")
                 .append(alloc.line().append(e.pretty(alloc, env)).nest(2).append(alloc.line_()))
                 .group(),
-            Exp::Forall(binders, box exp) => alloc
+            Exp::Forall(binders, trig, box exp) => alloc
                 .text("forall ")
                 .append(alloc.intersperse(
                     binders.iter().map(|(b, t)| {
@@ -738,9 +754,10 @@ impl Print for Exp {
                     }),
                     ", ",
                 ))
+                .append(trig.pretty(alloc, env))
                 .append(" . ")
                 .append(exp.pretty(alloc, env)),
-            Exp::Exists(binders, box exp) => alloc
+            Exp::Exists(binders, trig, box exp) => alloc
                 .text("exists ")
                 .append(alloc.intersperse(
                     binders.iter().map(|(b, t)| {
@@ -748,6 +765,7 @@ impl Print for Exp {
                     }),
                     ", ",
                 ))
+                .append(trig.pretty(alloc, env))
                 .append(" . ")
                 .append(exp.pretty(alloc, env)),
             Exp::Impl(box hyp, box exp) => {