File tree Expand file tree Collapse file tree 3 files changed +6
-10
lines changed
examples/solidity/GradualPonzi
vscode/quint-vscode/server Expand file tree Collapse file tree 3 files changed +6
-10
lines changed Original file line number Diff line number Diff line change @@ -232,7 +232,7 @@ module gradualPonziTest {
232232 //
233233 // If quint has not reported a violation, try:
234234 //
235- // $ quint run --invariant=progressInv --main=gradualPonziTest --seed=0x8385bfe3a7497 gradualPonzi.qnt
235+ // $ quint run --invariant=progressInv --main=gradualPonziTest --max-steps=50 -- seed=0x8272b36d6a57f gradualPonzi.qnt
236236 //
237237 // It is quite hard for `quint run` to find a violation to this property.
238238 // In contrast, `quint verify` finds it in a few seconds.
@@ -254,4 +254,4 @@ module gradualPonziTest {
254254 val sumRewards = addr.fold( 0 , ( s, a) = > s + ponziState.rewards.get( a))
255255 sumRewards == evmState.balances.get( " contract" )
256256 }
257- }
257+ }
Original file line number Diff line number Diff line change 319319 --invariant=noNegativeInv --main=gradualPonziTest \
320320 ../examples/solidity/GradualPonzi/gradualPonzi.qnt
321321
322- ### IGNORE on run gradualPonzi::progressInv
322+ ### FAIL on run gradualPonzi::progressInv
323323
324- This test should fail. We know that from ` quint verify ` .
325- However, ` quint run ` has hard time finding a counterexample.
326- If you see this test failing, you are a lucky winner!
327- Add the seed to the command below and change the exit code to 1.
328-
329- <!-- !test exit 0 -->
324+ <!-- !test exit 1 -->
330325<!-- !test check gradualPonzi - Run progressInv -->
331326 quint run --invariant=progressInv --main=gradualPonziTest \
332327 --max-samples=1000 --max-steps=50 \
328+ --seed=0x8272b36d6a57f \
333329 ../examples/solidity/GradualPonzi/gradualPonzi.qnt
334330
335331### FAIL on run gradualPonzi::noLeftoversInv
Original file line number Diff line number Diff line change 11{
2- "name" : " quint-language-server" ,
2+ "name" : " @informalsystems/ quint-language-server" ,
33 "description" : " Language Server for the Quint specification language" ,
44 "version" : " 0.8.0" ,
55 "author" : " Informal Systems" ,
You can’t perform that action at this time.
0 commit comments