fix: handle assert for ensures on spec functions

Author: Marsman1996

source/vir/src/sst_to_air_func.rs

@@ -10,7 +10,7 @@ use crate::def::{
     prefix_fuel_nat, prefix_no_unwind_when, prefix_open_inv, prefix_pre_var, prefix_recursive_fun,
     prefix_requires, static_name, suffix_global_id, suffix_typ_param_ids,
 };
-use crate::messages::{MessageLabel, Span};
+use crate::messages::{MessageLabel, Span, internal_error};
 use crate::sst::FuncCheckSst;
 use crate::sst::{BndX, ExpX, Exps, FunctionSst, ParPurpose, ParX, Pars};
 use crate::sst_to_air::{
@@ -698,7 +698,12 @@ pub fn func_decl_to_air(ctx: &mut Ctx, function: &FunctionSst) -> Result<Command
             }
         }
     } else {
-        assert!(!function.x.has.has_ensures); // no ensures allowed on spec functions yet
+        if function.x.has.has_ensures {
+            return Err(crate::messages::error(
+                &function.x.ret.span,
+                "no ensures allowed on spec functions yet",
+            ));
+        }
     }
 
     if is_trait_method_impl {