Unable to run docker script

[guialvares]

trafficstars

When I tried to run the example of Readme at Docker directory, I got an error:

I also commented on the second line of Annotations.sol, so there is not this pragma solidity >=0.7.0; anymore.

 ./runsv.sh ../test/solc-verify/examples/Annotations.sol

++ realpath ../test/solc-verify/examples/Annotations.sol
+ ABSPATH=/home/guilherme/testing/solidity/test/solc-verify/examples/Annotations.sol
++ dirname /home/guilherme/testing/solidity/test/solc-verify/examples/Annotations.sol
+ DIR=/home/guilherme/testing/solidity/test/solc-verify/examples
++ basename /home/guilherme/testing/solidity/test/solc-verify/examples/Annotations.sol
+ FILE=/host/Annotations.sol
+ shift
+ docker run -it --rm --mount type=bind,source=/home/guilherme/testing/solidity/test/solc-verify/examples,target=/host solc-verify:latest /host/Annotations.sol
Error while running verifier, details:
----- Verifier output -----
*** Error: '/nologo': Filename extension '' is not supported. Input files must be BoogiePL programs (.bpl).

---------------------------
Error while running verifier, details:
Error while running verifier, details:
----- Verifier output -----
----- Verifier output -----
*** Error: '/nologo': Filename extension '' is not supported. Input files must be BoogiePL programs (.bpl).
*** Error: '/nologo': Filename extension '' is not supported. Input files must be BoogiePL programs (.bpl).


---------------------------
---------------------------
Error while running verifier, details:
----- Verifier output -----
*** Error: '/nologo': Filename extension '' is not supported. Input files must be BoogiePL programs (.bpl).

---------------------------
C::add_to_x: ERROR
C::add: ERROR
C::[implicit_constructor]: ERROR
C::[receive_ether_selfdestruct]: ERROR
Use --show-warnings to see 2 warnings.
Errors were found by the verifier.