From 519379f6ee1318144a050c99d82ef54b47ba79f2 Mon Sep 17 00:00:00 2001 From: dewert99 Date: Fri, 20 Oct 2023 09:41:51 -0700 Subject: [PATCH] Fixed type-invariant triggers to also depend on option --- creusot/src/backend/ty_inv.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/creusot/src/backend/ty_inv.rs b/creusot/src/backend/ty_inv.rs index 863cbe1e7d..2d6337b2bd 100644 --- 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 }