Hevm equivalence check throwing an error

[tushar994]

The command I am running is

hevm equivalence --code-a 608060405234801561000f575f5ffd5b5060043610610034575f3560e01c80633fb5c1cb146100385780638381f58a14610054575b5f5ffd5b610052600480360381019061004d91906100c8565b610072565b005b61005c61008c565b6040516100699190610102565b60405180910390f35b805f5f8282546100829190610148565b9250508190555050565b5f5481565b5f5ffd5b5f819050919050565b6100a781610095565b81146100b1575f5ffd5b50565b5f813590506100c28161009e565b92915050565b5f602082840312156100dd576100dc610091565b5b5f6100ea848285016100b4565b91505092915050565b6100fc81610095565b82525050565b5f6020820190506101155f8301846100f3565b92915050565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b5f61015282610095565b915061015d83610095565b92508282019050808211156101755761017461011b565b5b9291505056fea2646970667358221220d3af46c99e5d9e0fc933da0a569d75413330778d3a2e28db122e27fb3f236d4164736f6c634300081d0033 --code-b 608060405234801561000f575f5ffd5b5060043610610034575f3560e01c80633fb5c1cb146100385780638381f58a14610054575b5f5ffd5b610052600480360381019061004d9190610142565b610072565b005b61005c610106565b604051610069919061017c565b60405180910390f35b5f81905060038161008391906101ef565b5f5f828254610092919061021f565b925050819055506003816100a691906101ef565b5f5f8282546100b5919061021f565b925050819055506003816100c991906101ef565b5f5f8282546100d8919061021f565b925050819055506003816100ec9190610252565b5f5f8282546100fb919061021f565b925050819055505050565b5f5481565b5f5ffd5b5f819050919050565b6101218161010f565b811461012b575f5ffd5b50565b5f8135905061013c81610118565b92915050565b5f602082840312156101575761015661010b565b5b5f6101648482850161012e565b91505092915050565b6101768161010f565b82525050565b5f60208201905061018f5f83018461016d565b92915050565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52601260045260245ffd5b7f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b5f6101f98261010f565b91506102048361010f565b92508261021457610213610195565b5b828204905092915050565b5f6102298261010f565b91506102348361010f565b925082820190508082111561024c5761024b6101c2565b5b92915050565b5f61025c8261010f565b91506102678361010f565b92508261027757610276610195565b5b82820690509291505056fea2646970667358221220477ea9032b5db6339f130d329d1be8b73d69bb61eed4ebf7fb82c1dbac264a6b64736f6c634300081d0033

The two contracts it is checking equivalence for is

// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.13;

contract MyContract {
    uint256 public number=1;

    function setNumber(uint256 newNumber) public {
        number += newNumber;
    }
}

and

// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.13;

contract MyContract {
    uint256 public number=1;

    function setNumber(uint256 newNumber) public {
        uint256 newNumber2 = newNumber;
        number += (newNumber2/3);
        number += (newNumber2/3);
        number += (newNumber2/3);
        number += (newNumber2%3);
    }
}

I compiled and got the bytecodes for the two files using solc --bin-runtime "file.sol" | tail -n1.

The error I get is

Found 70 total pairs of endstates
Asking the SMT solver for 50 pairs

Reuse of previous queries was Useful in 0 cases
No discrepancies found
But the following issues occurred:
      4x -> SMT result timeout/unknown

am I doing something wrong?

[msooseth]

Hey, Just a quick feedback (it’s late here) have you tried with bitwuza? Just call it with —solver bitwuzla and have bitwuzla installed/in your PATH. Otherwise you can also increase the time limit (—smt-time-limit) from the default 100. Hit bitwuzla is sooo much faster than the default z3 solver :) Good luck and I’ll get back to you tomorrow, Mate

…

On Wed 9. Apr 2025 at 19:23, Tushar Jain ***@***.***> wrote: The command I am running is hevm equivalence --code-a 608060405234801561000f575f5ffd5b5060043610610034575f3560e01c80633fb5c1cb146100385780638381f58a14610054575b5f5ffd5b610052600480360381019061004d91906100c8565b610072565b005b61005c61008c565b6040516100699190610102565b60405180910390f35b805f5f8282546100829190610148565b9250508190555050565b5f5481565b5f5ffd5b5f819050919050565b6100a781610095565b81146100b1575f5ffd5b50565b5f813590506100c28161009e565b92915050565b5f602082840312156100dd576100dc610091565b5b5f6100ea848285016100b4565b91505092915050565b6100fc81610095565b82525050565b5f6020820190506101155f8301846100f3565b92915050565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b5f61015282610095565b915061015d83610095565b92508282019050808211156101755761017461011b565b5b9291505056fea2646970667358221220d3af46c99e5d9e0fc933da0a569d75413330778d3a2e28db122e27fb3f236d4164736f6c634300081d0033 --code-b 608060405234801561000f575f5ffd5b5060043610610034575f3560e01c80633fb5c1cb146100385780638381f58a14610054575b5f5ffd5b610052600480360381019061004d9190610142565b610072565b005b61005c610106565b604051610069919061017c565b60405180910390f35b5f81905060038161008391906101ef565b5f5f828254610092919061021f565b925050819055506003816100a691906101ef565b5f5f8282546100b5919061021f565b925050819055506003816100c991906101ef565b5f5f8282546100d8919061021f565b925050819055506003816100ec9190610252565b5f5f8282546100fb919061021f565b925050819055505050565b5f5481565b5f5ffd5b5f819050919050565b6101218161010f565b811461012b575f5ffd5b50565b5f8135905061013c81610118565b92915050565b5f602082840312156101575761015661010b565b5b5f6101648482850161012e565b91505092915050565b6101768161010f565b82525050565b5f60208201905061018f5f83018461016d565b92915050565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52601260045260245ffd5b7f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b5f6101f98261010f565b91506102048361010f565b92508261021457610213610195565b5b828204905092915050565b5f6102298261010f565b91506102348361010f565b925082820190508082111561024c5761024b6101c2565b5b92915050565b5f61025c8261010f565b91506102678361010f565b92508261027757610276610195565b5b82820690509291505056fea2646970667358221220477ea9032b5db6339f130d329d1be8b73d69bb61eed4ebf7fb82c1dbac264a6b64736f6c634300081d0033 The two contracts it is checking equivalence for is // SPDX-License-Identifier: UNLICENSED pragma solidity ^0.8.13; contract MyContract { uint256 public number=1; function setNumber(uint256 newNumber) public { number += newNumber; } } and // SPDX-License-Identifier: UNLICENSED pragma solidity ^0.8.13; contract MyContract { uint256 public number=1; function setNumber(uint256 newNumber) public { uint256 newNumber2 = newNumber; number += (newNumber2/3); number += (newNumber2/3); number += (newNumber2/3); number += (newNumber2%3); } } I compiled and got the bytecodes for the two files using solc --bin-runtime "file.sol" | tail -n1. The error I get is Found 70 total pairs of endstates Asking the SMT solver for 50 pairs Reuse of previous queries was Useful in 0 cases No discrepancies found But the following issues occurred: 4x -> SMT result timeout/unknown am I doing something wrong? — Reply to this email directly, view it on GitHub <#704>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AXYLY5HINSOSC6XAXC6UKHT2YVJS7AVCNFSM6AAAAAB2ZRZRHSVHI2DSMVQWIX3LMV43ASLTON2WKOZSHE4DGNBUGA2DMMY> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***> *tushar994* created an issue (ethereum/hevm#704) <#704> The command I am running is hevm equivalence --code-a 608060405234801561000f575f5ffd5b5060043610610034575f3560e01c80633fb5c1cb146100385780638381f58a14610054575b5f5ffd5b610052600480360381019061004d91906100c8565b610072565b005b61005c61008c565b6040516100699190610102565b60405180910390f35b805f5f8282546100829190610148565b9250508190555050565b5f5481565b5f5ffd5b5f819050919050565b6100a781610095565b81146100b1575f5ffd5b50565b5f813590506100c28161009e565b92915050565b5f602082840312156100dd576100dc610091565b5b5f6100ea848285016100b4565b91505092915050565b6100fc81610095565b82525050565b5f6020820190506101155f8301846100f3565b92915050565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b5f61015282610095565b915061015d83610095565b92508282019050808211156101755761017461011b565b5b9291505056fea2646970667358221220d3af46c99e5d9e0fc933da0a569d75413330778d3a2e28db122e27fb3f236d4164736f6c634300081d0033 --code-b 608060405234801561000f575f5ffd5b5060043610610034575f3560e01c80633fb5c1cb146100385780638381f58a14610054575b5f5ffd5b610052600480360381019061004d9190610142565b610072565b005b61005c610106565b604051610069919061017c565b60405180910390f35b5f81905060038161008391906101ef565b5f5f828254610092919061021f565b925050819055506003816100a691906101ef565b5f5f8282546100b5919061021f565b925050819055506003816100c991906101ef565b5f5f8282546100d8919061021f565b925050819055506003816100ec9190610252565b5f5f8282546100fb919061021f565b925050819055505050565b5f5481565b5f5ffd5b5f819050919050565b6101218161010f565b811461012b575f5ffd5b50565b5f8135905061013c81610118565b92915050565b5f602082840312156101575761015661010b565b5b5f6101648482850161012e565b91505092915050565b6101768161010f565b82525050565b5f60208201905061018f5f83018461016d565b92915050565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52601260045260245ffd5b7f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b5f6101f98261010f565b91506102048361010f565b92508261021457610213610195565b5b828204905092915050565b5f6102298261010f565b91506102348361010f565b925082820190508082111561024c5761024b6101c2565b5b92915050565b5f61025c8261010f565b91506102678361010f565b92508261027757610276610195565b5b82820690509291505056fea2646970667358221220477ea9032b5db6339f130d329d1be8b73d69bb61eed4ebf7fb82c1dbac264a6b64736f6c634300081d0033 The two contracts it is checking equivalence for is // SPDX-License-Identifier: UNLICENSED pragma solidity ^0.8.13; contract MyContract { uint256 public number=1; function setNumber(uint256 newNumber) public { number += newNumber; } } and // SPDX-License-Identifier: UNLICENSED pragma solidity ^0.8.13; contract MyContract { uint256 public number=1; function setNumber(uint256 newNumber) public { uint256 newNumber2 = newNumber; number += (newNumber2/3); number += (newNumber2/3); number += (newNumber2/3); number += (newNumber2%3); } } I compiled and got the bytecodes for the two files using solc --bin-runtime "file.sol" | tail -n1. The error I get is Found 70 total pairs of endstates Asking the SMT solver for 50 pairs Reuse of previous queries was Useful in 0 cases No discrepancies found But the following issues occurred: 4x -> SMT result timeout/unknown am I doing something wrong? — Reply to this email directly, view it on GitHub <#704>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AXYLY5HINSOSC6XAXC6UKHT2YVJS7AVCNFSM6AAAAAB2ZRZRHSVHI2DSMVQWIX3LMV43ASLTON2WKOZSHE4DGNBUGA2DMMY> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[blishko]

Also a quick feedback. What you are seeing is not hevm throwing an error.
It is just reporting results of the equivalence check.
It says it did not find a way to show non-equivalence (No discrepancies found), but there were some possibilities which it was not able to explore fully (But the following issues occurred: 4x -> SMT result timeout/unknown), so it cannot guarantee that the bytecodes are indeed equivalent in all cases.

[tushar994]

ahhh got it, thank you both so so much!!

[msooseth]

Glad to hear we could help. Let us know how your experience was with hevm -- if you have any feedback, we'd be happy to hear it, just open an issue for anything specific you found. In the meanwhile, if this issue has been resolved, let us know, so we can close it :)

Cheers and thanks again,

Mate