diff --git a/tests/difference/core/quint_model/README.md b/tests/difference/core/quint_model/README.md
index 66e34fd947..a2f66945b4 100644
--- a/tests/difference/core/quint_model/README.md
+++ b/tests/difference/core/quint_model/README.md
@@ -52,8 +52,8 @@ that were running at the time the packet was sent (and are still running).
 
 Invariants can also be model-checked by Apalache, using this command:
 ```
-quint verify --invariant ValidatorUpdatesArePropagated,ValidatorSetHasExistedInv,SameVSCPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv --main CCVDefaultState
-Machine ccv_statemachine.qnt
+quint verify --invariant ValidatorUpdatesArePropagated,ValidatorSetHasExistedInv,SameVSCPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv \
+--main CCVDefaultStateMachine ccv_statemachine.qnt
 ```
 
 ### Sanity Checks