From 8aee401634dfafc918044a8ce459898f02b562a9 Mon Sep 17 00:00:00 2001
From: Philip Offtermatt
Date: Wed, 11 Oct 2023 11:48:46 +0200
Subject: [PATCH] Fix voting power change behaviour around 0
---
tests/difference/core/quint_model/ccv.qnt | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt
index 2b975d6c53..606574c42b 100644
--- a/tests/difference/core/quint_model/ccv.qnt
+++ b/tests/difference/core/quint_model/ccv.qnt
@@ -250,8 +250,8 @@ module ccv {
// the power of a validator on the provider chain is changed to the given amount. We do not care how this happens,
// e.g. via undelegations, or delegations, ...
pure def votingPowerChange(currentState: ProtocolState, validator: Node, amount: int): Result = {
- if (amount <= 0) {
- Err("Voting power changes must be positive")
+ if (amount < 0) {
+ Err("Voting power changes must be nonnegative")
} else {
pure val currentValidatorSet = currentState.providerState.chainState.currentValidatorSet
pure val newValidatorSet = getUpdatedValidatorSet(currentValidatorSet, validator, amount)