More fixes

programs/manifest/src/certora/spec/cancel_order_checks.rs

@@ -122,7 +122,6 @@ pub fn cancel_order_by_index_no_revert<const IS_BID: bool>() {
     // -- call to cancel_order_by_index
     let market_data = &mut market_info.try_borrow_mut_data().unwrap();
     let mut dynamic_account: MarketRefMut = get_mut_dynamic_account(market_data);
-    let trader_index = crate::state::second_trader_index();
     let order_index = maker_order_index;
     let result = dynamic_account.cancel_order_by_index(order_index, &[None, None]);
     cvt_assert!(result.is_ok());

programs/manifest/src/certora/spec/funds_checks.rs

@@ -371,7 +371,6 @@ pub fn cancel_order_by_index_check<const IS_BID: bool>() {
     cvt_assume_funds_invariants(balances_old);
 
     // -- call to cancel_order_by_index
-    let trader_index = second_trader_index();
     let order_index = maker_order_index;
     cancel_order_by_index!(market_info, order_index);
 

programs/manifest/src/certora/spec/matching_checks.rs

@@ -446,7 +446,7 @@ pub fn matching_decrease_maker_order_atoms<const IS_BID: bool>() {
         place_single_order_nondet_inputs::<IS_BID>(market_info);
 
     // -- call to place_single_order
-    let (res, _total_base_atoms_traded, _total_quote_atoms_traded) = place_single_order!(
+    let (_res, _total_base_atoms_traded, _total_quote_atoms_traded) = place_single_order!(
         market_info,
         args,
         remaining_base_atoms,

programs/manifest/src/state/global.rs

@@ -11,7 +11,6 @@ use hypertree::{
     get_helper, get_mut_helper, DataIndex, FreeList, Get, HyperTreeReadOperations,
     HyperTreeWriteOperations, RBNode, RedBlackTree, RedBlackTreeReadOnly, NIL,
 };
-
 use shank::ShankType;
 use solana_program::{entrypoint::ProgramResult, program_error::ProgramError, pubkey::Pubkey};
 use static_assertions::const_assert_eq;

programs/manifest/src/validation/loaders.rs

@@ -466,7 +466,11 @@ impl<'a, 'info> BatchUpdateContext<'a, 'info> {
             ManifestAccountInfo::<MarketFixed>::new(next_account_info(account_iter)?)?;
         let system_program: Program =
             Program::new(next_account_info(account_iter)?, &system_program::id())?;
-
+        // Certora version is not mutable.
+        #[cfg(feature = "certora")]
+        let global_trade_accounts_opts: [Option<GlobalTradeAccounts<'a, 'info>>; 2] =
+            [None, None];
+        #[cfg(not(feature = "certora"))]
         let mut global_trade_accounts_opts: [Option<GlobalTradeAccounts<'a, 'info>>; 2] =
             [None, None];