VeriSol translation error - Expecting a call of the form e.send/e.transfer/e.call, but found transfer(msg.sender, _to, _value)

[syscoopco]

My contract successfully compiles on truffle, and the code doesn't exhibit any problems during unit testing. Below are the faulty command and code:

COMMAND LINE:

$ VeriSol /home/user/work/verisol/ManicatoTokenVeriSol.sol ManicatoToken Command line args = {/home/user/work/verisol/ManicatoTokenVeriSol.sol, ManicatoToken} SpecFilesDir = /home/user/work/verisol ... running Solc on /home/user/work/verisol/ManicatoTokenVeriSol.sol ... running SolToBoogie to translate Solidity to Boogie Warning: A mapping with complex value type allowances of valuetype mapping (address => uint256) VeriSol translation error: File /home/user/work/verisol/ManicatoTokenVeriSol.sol, Line 475, Contract ManicatoToken, Function transfer:: Expecting a call of the form e.send/e.transfer/e.call, but found transfer(msg.sender, _to, _value)....

CODE (buggy line in bold):

...

function transfer(address _from, address _to, uint256 _value) internal returns (bool success){

    uint valueX100 = SafeMath.mul(_value, 100);
    require(valueX100 <= accounts[_from].releasedMANX100, "Insufficient released manicatos to transfer.");
    accounts[_from].releasedMANX100 = SafeMath.sub(accounts[_from].releasedMANX100, valueX100);
    accounts[_to].releasedMANX100 = SafeMath.add(accounts[_to].releasedMANX100, valueX100);
    emit Transfer(_from, _to, _value);
    return true;
}

function transfer(address _to, uint256 _value) public returns (bool success) {

    **return transfer(msg.sender, _to, _value);**
}

...

[shuvendu-lahiri]

I think this is a known issue #157 given there are two functions named transfer.

[syscoopco]

You're right. Thanks.