From e9d7107a44a24fe1ca4ff29d7d6d789245df5b1b Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Wed, 8 Nov 2023 14:12:42 +0100 Subject: [PATCH] Adjust max steps and run all tests --- tests/difference/core/quint_model/run_invariants.sh | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tests/difference/core/quint_model/run_invariants.sh b/tests/difference/core/quint_model/run_invariants.sh index 4c65693cc0..03e63db579 100755 --- a/tests/difference/core/quint_model/run_invariants.sh +++ b/tests/difference/core/quint_model/run_invariants.sh @@ -1,4 +1,5 @@ #! /bin/sh quint test ccv_model.qnt -quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" ccv_model.qnt --max-steps 500 --max-samples 200 \ No newline at end of file +quint test ccv_test.qnt +quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" ccv_model.qnt --max-steps 200 --max-samples 200 \ No newline at end of file