diff --git a/tests/difference/core/quint_model/README.md b/tests/difference/core/quint_model/README.md index 696cb183a9..503bf9ee5e 100644 --- a/tests/difference/core/quint_model/README.md +++ b/tests/difference/core/quint_model/README.md @@ -56,6 +56,4 @@ The available sanity checks are: - CanStopConsumer - CanTimeoutConsumer - CanSendVSCPackets -- CanSendVSCMaturedPackets - -Run all sanity checks by running `run_sanity_checks.sh`. \ No newline at end of file +- CanSendVSCMaturedPackets \ No newline at end of file diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt index 7d9edf884e..d557da1b5a 100644 --- a/tests/difference/core/quint_model/ccv.qnt +++ b/tests/difference/core/quint_model/ccv.qnt @@ -457,9 +457,9 @@ module CCV { "currentValidatorSet", providerStateAfterConsumerAdvancement.chainState.currentValidatorSet ) ) - (consumer, newConsumerState) + newConsumerState } else { - (consumer, currentState.consumerStates.get(consumer)) + currentState.consumerStates.get(consumer) } ) val newState = currentState.with( diff --git a/tests/difference/core/quint_model/run_sanity_checks.sh b/tests/difference/core/quint_model/run_sanity_checks.sh deleted file mode 100755 index 546d5468f1..0000000000 --- a/tests/difference/core/quint_model/run_sanity_checks.sh +++ /dev/null @@ -1 +0,0 @@ -quint run --invariant "all{CanRunConsumer,CanStopConsumer,CanTimeoutConsumer,CanSendVSCPackets,CanSendVSCMaturedPackets}" ccv_statemachine.qnt --main CCVDefaultStateMachine --max-steps 2000 --max-samples 200 \ No newline at end of file