search

microsoft / verisol

A formal verifier and analysis tool for Solidity Smart Contracts
Other
245 stars 46 forks source link

Dump Boogie/SMT-LIB #217

Closed yoni206 closed 4 years ago

yoni206 commented 4 years ago

Is there a way to dump the Boogie / SMT-LIB intermediate files that are generated by VeriSol?

shuvendu-lahiri commented 4 years ago

When you run VeriSol, there is a Boogie file __SolToBoogieTest_out.bpl that is generated in the same folder. 

dotnet d:\verisol\bin\debug\verisol.dll Error.sol AssertFalse

You can generate the SMT-LIB formula by running Boogie.