microsoft / verisol

A formal verifier and analysis tool for Solidity Smart Contracts

Other

245 stars 46 forks source link

Open suvamM opened 5 years ago

suvamM commented 5 years ago

With the latest VeriSol version, Corral throws the following error while checking the generated Boogie file:

Error, internal bug: Refinement unable to make progress.

The input Solidity file has not been changed.

shuvendu-lahiri commented 5 years ago

This is most likely related to the lack of trigger for quantifiers. Working on a fix offline.

shuvendu-lahiri commented 5 years ago

114 does not resolve the issue by itself.

shuvendu-lahiri commented 4 years ago

Repro (from Diego)

VeriSol ERC20-nosafemath.sol ERC20 /useModularArithmetic