Avoided replacing trigger for any function that returns ()

creusot-rs · Oct 20, 2023 · 5b3e8e3 · 5b3e8e3
1 parent 79db07c
commit 5b3e8e3
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/creusot/src/backend/signature.rs b/creusot/src/backend/signature.rs
@@ -2,6 +2,7 @@ use rustc_hir::{def::Namespace, def_id::DefId};
 use why3::{
     declaration::{Contract, Signature},
     exp::{Binder, Trigger},
+    ty::Type,
 };
 
 use crate::{
@@ -65,7 +66,10 @@ pub(crate) fn sig_to_why3<'tcx>(
 
     let retty = names
         .with_public_clones(|names| backend::ty::translate_ty(ctx, names, span, pre_sig.output));
-    let trigger = if ctx.opts.simple_triggers && should_replace_trigger(ctx.tcx, def_id) {
+    let trigger = if ctx.opts.simple_triggers
+        && should_replace_trigger(ctx.tcx, def_id)
+        && retty != Type::UNIT
+    {
         None
     } else {
         Some(Trigger::NONE)