Fixed type-invariant triggers to also depend on option

creusot-rs · Oct 20, 2023 · 519379f · 519379f
1 parent 41dfd92
commit 519379f
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/creusot/src/backend/ty_inv.rs b/creusot/src/backend/ty_inv.rs
@@ -187,10 +187,12 @@ 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_trig(
         vec![("self".into(), translate_ty(ctx, names, DUMMY_SP, ty))],
-        Trigger::single(lhs.clone()),
+        trigger,
         lhs.eq(rhs),
     );
     Axiom { name, rewrite: !trivial, axiom }