Long Contract - Remove Commit NEXT statements when that variable is not used

The file data/regression/supported_features/SimpleFunction2.sol is easy and should be solved very quickly, but it does not. I suspect that this is due to the require statement commit stage being added to every function regardless of if there is a require statement, but I do not know for sure.
The goal of this issue is to get SimpleFunction2 working in under a minute.
See the SMV output from this command: -debug -loglevel debug -run solve -input data/regression/supported_features/SimpleFunction2.sol !x
MODULE main
VAR
NuSMVState : {
    start,SimpleFunction2_constructor_ConstructorEntryState_ln0,SimpleFunction2_constructor_DataChangeState_ln1,SimpleFunction2_constructor_FunctionSuccessState_ln2,LoopState,SimpleFunction2_func1_FunctionEntryState_ln0,SimpleFunction2_func2a_FunctionEntryState_ln0,SimpleFunction2_func2aa_FunctionEntryState_ln0,SimpleFunction2_func2aaa_FunctionEntryState_ln0,SimpleFunction2_func3_FunctionEntryState_ln0,SimpleFunction2_func4_FunctionEntryState_ln0,SimpleFunction2__FunctionEntryState_ln0,SimpleFunction2_func1_FunctionSuccessState_ln1,SimpleFunction2_func2a_DataChangeState_ln1,SimpleFunction2_func2aa_DataChangeState_ln1,SimpleFunction2_func2aaa_DataChangeState_ln1,SimpleFunction2_func3_DataChangeState_ln1,SimpleFunction2_func4_FunctionSuccessState_ln1,SimpleFunction2__FunctionSuccessState_ln1,SimpleFunction2_func2a_DataChangeState_ln2,SimpleFunction2_func2aa_DataChangeState_ln2,SimpleFunction2_func2aaa_DataChangeState_ln2,SimpleFunction2_func3_FunctionSuccessState_ln2,SimpleFunction2_func2a_DataChangeState_ln3,SimpleFunction2_func2aa_DataChangeState_ln3,SimpleFunction2_func2aaa_DataChangeState_ln3,SimpleFunction2_func2a_FunctionSuccessState_ln4,SimpleFunction2_func2aa_FunctionSuccessState_ln4,SimpleFunction2_func2aaa_FunctionSuccessState_ln4
};
__QueryName : {
    ValueReachabilityQuery_0,ValueReachabilityQuery_1,ValueReachabilityQuery_2,ValueReachabilityQuery_3,ValueReachabilityQuery_4,ValueReachabilityQuery_5,ValueReachabilityQuery_6,ValueReachabilityQuery_7,ValueReachabilityQuery_8,ValueReachabilityQuery_9,ValueReachabilityQuery_10,ValueReachabilityQuery_11
};
contract1 : contract_SimpleFunction2(NuSMVState,__QueryName);
IVAR
nextFunc : {LoopState,SimpleFunction2_func1_FunctionEntryState_ln0,SimpleFunction2_func2a_FunctionEntryState_ln0,SimpleFunction2_func2aa_FunctionEntryState_ln0,SimpleFunction2_func2aaa_FunctionEntryState_ln0,SimpleFunction2_func3_FunctionEntryState_ln0,SimpleFunction2_func4_FunctionEntryState_ln0,SimpleFunction2__FunctionEntryState_ln0};
ASSIGN
init(NuSMVState) := start;
next(NuSMVState) := case
    NuSMVState = LoopState : nextFunc;
    NuSMVState = start : SimpleFunction2_constructor_ConstructorEntryState_ln0;
    NuSMVState = SimpleFunction2_constructor_ConstructorEntryState_ln0 : SimpleFunction2_constructor_DataChangeState_ln1;
    NuSMVState = SimpleFunction2_constructor_DataChangeState_ln1 : SimpleFunction2_constructor_FunctionSuccessState_ln2;
    NuSMVState = SimpleFunction2_constructor_FunctionSuccessState_ln2 : LoopState;
    NuSMVState = SimpleFunction2_func1_FunctionEntryState_ln0 : SimpleFunction2_func1_FunctionSuccessState_ln1;
    NuSMVState = SimpleFunction2_func2a_FunctionEntryState_ln0 : SimpleFunction2_func2a_DataChangeState_ln1;
    NuSMVState = SimpleFunction2_func2aa_FunctionEntryState_ln0 : SimpleFunction2_func2aa_DataChangeState_ln1;
    NuSMVState = SimpleFunction2_func2aaa_FunctionEntryState_ln0 : SimpleFunction2_func2aaa_DataChangeState_ln1;
    NuSMVState = SimpleFunction2_func3_FunctionEntryState_ln0 : SimpleFunction2_func3_DataChangeState_ln1;
    NuSMVState = SimpleFunction2_func4_FunctionEntryState_ln0 : SimpleFunction2_func4_FunctionSuccessState_ln1;
    NuSMVState = SimpleFunction2__FunctionEntryState_ln0 : SimpleFunction2__FunctionSuccessState_ln1;
    NuSMVState = SimpleFunction2_func1_FunctionSuccessState_ln1 : LoopState;
    NuSMVState = SimpleFunction2_func2a_DataChangeState_ln1 : SimpleFunction2_func2a_DataChangeState_ln2;
    NuSMVState = SimpleFunction2_func2aa_DataChangeState_ln1 : SimpleFunction2_func2aa_DataChangeState_ln2;
    NuSMVState = SimpleFunction2_func2aaa_DataChangeState_ln1 : SimpleFunction2_func2aaa_DataChangeState_ln2;
    NuSMVState = SimpleFunction2_func3_DataChangeState_ln1 : SimpleFunction2_func3_FunctionSuccessState_ln2;
    NuSMVState = SimpleFunction2_func4_FunctionSuccessState_ln1 : LoopState;
    NuSMVState = SimpleFunction2__FunctionSuccessState_ln1 : LoopState;
    NuSMVState = SimpleFunction2_func2a_DataChangeState_ln2 : SimpleFunction2_func2a_DataChangeState_ln3;
    NuSMVState = SimpleFunction2_func2aa_DataChangeState_ln2 : SimpleFunction2_func2aa_DataChangeState_ln3;
    NuSMVState = SimpleFunction2_func2aaa_DataChangeState_ln2 : SimpleFunction2_func2aaa_DataChangeState_ln3;
    NuSMVState = SimpleFunction2_func3_FunctionSuccessState_ln2 : LoopState;
    NuSMVState = SimpleFunction2_func2a_DataChangeState_ln3 : SimpleFunction2_func2a_FunctionSuccessState_ln4;
    NuSMVState = SimpleFunction2_func2aa_DataChangeState_ln3 : SimpleFunction2_func2aa_FunctionSuccessState_ln4;
    NuSMVState = SimpleFunction2_func2aaa_DataChangeState_ln3 : SimpleFunction2_func2aaa_FunctionSuccessState_ln4;
    NuSMVState = SimpleFunction2_func2a_FunctionSuccessState_ln4 : LoopState;
    NuSMVState = SimpleFunction2_func2aa_FunctionSuccessState_ln4 : LoopState;
    NuSMVState = SimpleFunction2_func2aaa_FunctionSuccessState_ln4 : LoopState;
    TRUE: NuSMVState;
esac;

MODULE contract_SimpleFunction2(NuSMVState,__QueryName)
-- Smart Contract "SimpleFunction2" was generated from file: "D:\Work\Masters_Phd\workspace (GradSchool)\solidity-safety-to-model-checking\data\regression\supported_features\SimpleFunction2.sol"
-- Contract Number: 1
DEFINE
CTLSPEC NAME ValueReachabilityQuery_0 := AG !(__QueryName = ValueReachabilityQuery_0 & NuSMVState = LoopState & a = 10);
CTLSPEC NAME ValueReachabilityQuery_1 := AG !(__QueryName = ValueReachabilityQuery_1 & NuSMVState = LoopState & aa = 11);
CTLSPEC NAME ValueReachabilityQuery_2 := AG !(__QueryName = ValueReachabilityQuery_2 & NuSMVState = LoopState & aaa = 12);
CTLSPEC NAME ValueReachabilityQuery_3 := AG !(__QueryName = ValueReachabilityQuery_3 & NuSMVState = LoopState & a = 20);
CTLSPEC NAME ValueReachabilityQuery_4 := AG !(__QueryName = ValueReachabilityQuery_4 & NuSMVState = LoopState & aa = 31);
CTLSPEC NAME ValueReachabilityQuery_5 := AG !(__QueryName = ValueReachabilityQuery_5 & NuSMVState = LoopState & aaa = 42);
CTLSPEC NAME ValueReachabilityQuery_6 := AG !(__QueryName = ValueReachabilityQuery_6 & NuSMVState = LoopState & a = 11);
CTLSPEC NAME ValueReachabilityQuery_7 := AG !(__QueryName = ValueReachabilityQuery_7 & NuSMVState = LoopState & a = 12);
CTLSPEC NAME ValueReachabilityQuery_8 := AG !(__QueryName = ValueReachabilityQuery_8 & NuSMVState = LoopState & aa = 10);
CTLSPEC NAME ValueReachabilityQuery_9 := AG !(__QueryName = ValueReachabilityQuery_9 & NuSMVState = LoopState & aa = 12);
CTLSPEC NAME ValueReachabilityQuery_10 := AG !(__QueryName = ValueReachabilityQuery_10 & NuSMVState = LoopState & aaa = 10);
CTLSPEC NAME ValueReachabilityQuery_11 := AG !(__QueryName = ValueReachabilityQuery_11 & NuSMVState = LoopState & aaa = 11);
VAR
aa : 0 .. 200;
NuSMVTemp_aa : 0 .. 200;
aaa : 0 .. 200;
NuSMVTemp_aaa : 0 .. 200;
a : 0 .. 200;
NuSMVTemp_a : 0 .. 200;
total : 0 .. 200;
NuSMVTemp_total : 0 .. 200;
-- Function: function func2aa() private view returns(uint) 
a12 : 0 .. 200;
b22 : 0 .. 200;
-- Function: function func2a() private view returns(uint) 
a1 : 0 .. 200;
b2 : 0 .. 200;
-- Function: function func2aaa() private view returns(uint) 
a13 : 0 .. 200;
b23 : 0 .. 200;
-- Function: function func4(uint b) public view returns(bool) 
b : 0 .. 200;
ASSIGN
init(NuSMVTemp_aa) := 11;
init(aa) := 11;
init(NuSMVTemp_aaa) := 12;
init(aaa) := 12;
init(NuSMVTemp_a) := 10;
init(a) := 10;
init(NuSMVTemp_total) := 0;
init(total) := 0;
-- Function: function func2aa() private view returns(uint) 
init(a12) := 0;
init(b22) := 0;
-- Function: function func2a() private view returns(uint) 
init(a1) := 0;
init(b2) := 0;
-- Function: function func2aaa() private view returns(uint) 
init(a13) := 0;
init(b23) := 0;
next(NuSMVTemp_aa) := case
    NuSMVState = SimpleFunction2_func2aa_FunctionEntryState_ln0 : aa;
    NuSMVState = SimpleFunction2_func2aa_DataChangeState_ln3 : max(0, (NuSMVTemp_aa + 20) mod 200);
    NuSMVState = SimpleFunction2__FunctionEntryState_ln0 : aa;
    NuSMVState = SimpleFunction2_func2a_FunctionEntryState_ln0 : aa;
    NuSMVState = SimpleFunction2_func2aaa_FunctionEntryState_ln0 : aa;
    NuSMVState = SimpleFunction2_func4_FunctionEntryState_ln0 : aa;
    NuSMVState = SimpleFunction2_func1_FunctionEntryState_ln0 : aa;
    NuSMVState = SimpleFunction2_func3_FunctionEntryState_ln0 : aa;
    TRUE : NuSMVTemp_aa;
esac;
next(NuSMVTemp_aaa) := case
    NuSMVState = SimpleFunction2_func2aa_FunctionEntryState_ln0 : aaa;
    NuSMVState = SimpleFunction2__FunctionEntryState_ln0 : aaa;
    NuSMVState = SimpleFunction2_func2a_FunctionEntryState_ln0 : aaa;
    NuSMVState = SimpleFunction2_func2aaa_FunctionEntryState_ln0 : aaa;
    NuSMVState = SimpleFunction2_func2aaa_DataChangeState_ln3 : max(0, (NuSMVTemp_aaa + 30) mod 200);
    NuSMVState = SimpleFunction2_func4_FunctionEntryState_ln0 : aaa;
    NuSMVState = SimpleFunction2_func1_FunctionEntryState_ln0 : aaa;
    NuSMVState = SimpleFunction2_func3_FunctionEntryState_ln0 : aaa;
    TRUE : NuSMVTemp_aaa;
esac;
next(NuSMVTemp_a) := case
    NuSMVState = SimpleFunction2_func2aa_FunctionEntryState_ln0 : a;
    NuSMVState = SimpleFunction2__FunctionEntryState_ln0 : a;
    NuSMVState = SimpleFunction2_func2a_FunctionEntryState_ln0 : a;
    NuSMVState = SimpleFunction2_func2a_DataChangeState_ln3 : max(0, (NuSMVTemp_a + 10) mod 200);
    NuSMVState = SimpleFunction2_func2aaa_FunctionEntryState_ln0 : a;
    NuSMVState = SimpleFunction2_func4_FunctionEntryState_ln0 : a;
    NuSMVState = SimpleFunction2_func1_FunctionEntryState_ln0 : a;
    NuSMVState = SimpleFunction2_func3_FunctionEntryState_ln0 : a;
    TRUE : NuSMVTemp_a;
esac;
next(NuSMVTemp_total) := case
    NuSMVState = SimpleFunction2_func2aa_FunctionEntryState_ln0 : total;
    NuSMVState = SimpleFunction2__FunctionEntryState_ln0 : total;
    NuSMVState = SimpleFunction2_func2a_FunctionEntryState_ln0 : total;
    NuSMVState = SimpleFunction2_func2aaa_FunctionEntryState_ln0 : total;
    NuSMVState = SimpleFunction2_func4_FunctionEntryState_ln0 : total;
    NuSMVState = SimpleFunction2_func1_FunctionEntryState_ln0 : total;
    NuSMVState = SimpleFunction2_func3_FunctionEntryState_ln0 : total;
    NuSMVState = SimpleFunction2_func3_DataChangeState_ln1 : max(0, (total + 1) mod 200);
    TRUE : NuSMVTemp_total;
esac;
next(aa) := case
    NuSMVState = SimpleFunction2_constructor_FunctionSuccessState_ln2 : NuSMVTemp_aa;
    NuSMVState = SimpleFunction2_func2aa_FunctionSuccessState_ln4 : NuSMVTemp_aa;
    NuSMVState = SimpleFunction2__FunctionSuccessState_ln1 : NuSMVTemp_aa;
    NuSMVState = SimpleFunction2_func2a_FunctionSuccessState_ln4 : NuSMVTemp_aa;
    NuSMVState = SimpleFunction2_func2aaa_FunctionSuccessState_ln4 : NuSMVTemp_aa;
    NuSMVState = SimpleFunction2_func4_FunctionSuccessState_ln1 : NuSMVTemp_aa;
    NuSMVState = SimpleFunction2_func1_FunctionSuccessState_ln1 : NuSMVTemp_aa;
    NuSMVState = SimpleFunction2_func3_FunctionSuccessState_ln2 : NuSMVTemp_aa;
    TRUE : aa;
esac;
next(aaa) := case
    NuSMVState = SimpleFunction2_constructor_FunctionSuccessState_ln2 : NuSMVTemp_aaa;
    NuSMVState = SimpleFunction2_func2aa_FunctionSuccessState_ln4 : NuSMVTemp_aaa;
    NuSMVState = SimpleFunction2__FunctionSuccessState_ln1 : NuSMVTemp_aaa;
    NuSMVState = SimpleFunction2_func2a_FunctionSuccessState_ln4 : NuSMVTemp_aaa;
    NuSMVState = SimpleFunction2_func2aaa_FunctionSuccessState_ln4 : NuSMVTemp_aaa;
    NuSMVState = SimpleFunction2_func4_FunctionSuccessState_ln1 : NuSMVTemp_aaa;
    NuSMVState = SimpleFunction2_func1_FunctionSuccessState_ln1 : NuSMVTemp_aaa;
    NuSMVState = SimpleFunction2_func3_FunctionSuccessState_ln2 : NuSMVTemp_aaa;
    TRUE : aaa;
esac;
next(a) := case
    NuSMVState = SimpleFunction2_constructor_FunctionSuccessState_ln2 : NuSMVTemp_a;
    NuSMVState = SimpleFunction2_func2aa_FunctionSuccessState_ln4 : NuSMVTemp_a;
    NuSMVState = SimpleFunction2__FunctionSuccessState_ln1 : NuSMVTemp_a;
    NuSMVState = SimpleFunction2_func2a_FunctionSuccessState_ln4 : NuSMVTemp_a;
    NuSMVState = SimpleFunction2_func2aaa_FunctionSuccessState_ln4 : NuSMVTemp_a;
    NuSMVState = SimpleFunction2_func4_FunctionSuccessState_ln1 : NuSMVTemp_a;
    NuSMVState = SimpleFunction2_func1_FunctionSuccessState_ln1 : NuSMVTemp_a;
    NuSMVState = SimpleFunction2_func3_FunctionSuccessState_ln2 : NuSMVTemp_a;
    TRUE : a;
esac;
next(total) := case
    NuSMVState = SimpleFunction2_constructor_FunctionSuccessState_ln2 : NuSMVTemp_total;
    NuSMVState = SimpleFunction2_func2aa_FunctionSuccessState_ln4 : NuSMVTemp_total;
    NuSMVState = SimpleFunction2__FunctionSuccessState_ln1 : NuSMVTemp_total;
    NuSMVState = SimpleFunction2_func2a_FunctionSuccessState_ln4 : NuSMVTemp_total;
    NuSMVState = SimpleFunction2_func2aaa_FunctionSuccessState_ln4 : NuSMVTemp_total;
    NuSMVState = SimpleFunction2_func4_FunctionSuccessState_ln1 : NuSMVTemp_total;
    NuSMVState = SimpleFunction2_func1_FunctionSuccessState_ln1 : NuSMVTemp_total;
    NuSMVState = SimpleFunction2_func3_FunctionSuccessState_ln2 : NuSMVTemp_total;
    TRUE : total;
esac;
-- Function: function func2aa() private view returns(uint) 
next(a12) := case
    NuSMVState = SimpleFunction2_func2aa_FunctionEntryState_ln0 : a12;
    NuSMVState = SimpleFunction2_func2aa_DataChangeState_ln1 : 1;
    TRUE : a12;
esac;
next(b22) := case
    NuSMVState = SimpleFunction2_func2aa_FunctionEntryState_ln0 : b22;
    NuSMVState = SimpleFunction2_func2aa_DataChangeState_ln2 : 2;
    TRUE : b22;
esac;
-- Function: function func2a() private view returns(uint) 
next(a1) := case
    NuSMVState = SimpleFunction2_func2a_FunctionEntryState_ln0 : a1;
    NuSMVState = SimpleFunction2_func2a_DataChangeState_ln1 : 1;
    TRUE : a1;
esac;
next(b2) := case
    NuSMVState = SimpleFunction2_func2a_FunctionEntryState_ln0 : b2;
    NuSMVState = SimpleFunction2_func2a_DataChangeState_ln2 : 2;
    TRUE : b2;
esac;
-- Function: function func2aaa() private view returns(uint) 
next(a13) := case
    NuSMVState = SimpleFunction2_func2aaa_FunctionEntryState_ln0 : a13;
    NuSMVState = SimpleFunction2_func2aaa_DataChangeState_ln1 : 1;
    TRUE : a13;
esac;
next(b23) := case
    NuSMVState = SimpleFunction2_func2aaa_FunctionEntryState_ln0 : b23;
    NuSMVState = SimpleFunction2_func2aaa_DataChangeState_ln2 : 2;
    TRUE : b23;
esac;
-- Function: function func4(uint b) public view returns(bool) 
next(b) := case
    NuSMVState = SimpleFunction2_func4_FunctionEntryState_ln0 : b;
    TRUE : b;
esac;
Edited Mar 21, 2020 by Jon Shahen