From 45cfc5cd5414579221c45a9ec1c558d6ee4e558f Mon Sep 17 00:00:00 2001
From: Philip Offtermatt <p.offtermatt@gmail.com>
Date: Mon, 2 Oct 2023 11:03:08 +0200
Subject: [PATCH] Remove sanity check script

---
 tests/difference/core/quint_model/README.md            | 4 +---
 tests/difference/core/quint_model/ccv.qnt              | 4 ++--
 tests/difference/core/quint_model/run_sanity_checks.sh | 1 -
 3 files changed, 3 insertions(+), 6 deletions(-)
 delete mode 100755 tests/difference/core/quint_model/run_sanity_checks.sh

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