Merge pull request #1047 from informalsystems/th/fix-ex-simpleauction

Fix `SimpleAuction` example for dashboard

Author: Shon Feder

examples/README.md

@@ -88,7 +88,7 @@ listed without any additional command line arguments.
 | [solidity/ERC20/erc20.qnt](./solidity/ERC20/erc20.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [solidity/GradualPonzi/gradualPonzi.qnt](./solidity/GradualPonzi/gradualPonzi.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [solidity/icse23-fig7/lottery.qnt](./solidity/icse23-fig7/lottery.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
-| [solidity/SimpleAuction/SimpleAuctionNonComposable.qnt](./solidity/SimpleAuction/SimpleAuctionNonComposable.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
+| [solidity/SimpleAuction/SimpleAuction.qnt](./solidity/SimpleAuction/SimpleAuction.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
 | [solidity/SimplePonzi/simplePonzi.qnt](./solidity/SimplePonzi/simplePonzi.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [spells/basicSpells.qnt](./spells/basicSpells.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
 | [spells/commonSpells.qnt](./spells/commonSpells.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |

examples/solidity/SimpleAuction/SimpleAuctionNonComposable.qnt renamed to examples/solidity/SimpleAuction/SimpleAuction.qnt

@@ -80,7 +80,8 @@ module SimpleAuction {
     // No gas fees are taken into account.
     pure def evmSend(es: EvmState,
                      fromAddr: Addr, toAddr: Addr, value: int): EvmState = {
-        val bs = es.balances
+        // FIXME(#693): type annotation below is a workaround, inferred type is too general
+        val bs: Addr -> UInt = es.balances
         val fromBal = bs.get(fromAddr) - value
         val toBal = bs.get(toAddr) + value
         // compute the balances after `evmSend`

quint/cli-tests.md

@@ -187,10 +187,10 @@ Temporarily disabled.
 <!-- !test check coin - Types & Effects-->
     quint typecheck ../examples/solidity/Coin/coin.qnt
 
-### OK on test SimpleAuctionNonComposable.qnt
+### OK on test SimpleAuction.qnt
 
-<!-- !test check SimpleAuctionNonComposable - Syntax/Types & Effects/Unit tests -->
-    quint test --main=SimpleAuction ../examples/solidity/SimpleAuction/SimpleAuctionNonComposable.qnt
+<!-- !test check SimpleAuction - Syntax/Types & Effects/Unit tests -->
+    quint test ../examples/solidity/SimpleAuction/SimpleAuction.qnt
 
 ### OK on test lottery.qnt