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