search

secure-foundations / mariposa

MIT License
11 stars 7 forks source link

Updated convert-smtlib #22

Closed daneshvar-amrollahi closed 7 months ago

daneshvar-amrollahi commented 7 months ago

Hi,

My pull request includes the following upgrades:

  1. Added a new --incremental option for deciding whether to add (set-option :incremental true) when converting to SMT-LIB. The default value is False.
  2. Replace bv2int with bv2nat, which is the equivalent SMT-LIB function.
  3. Remove duplicate function definitions (such definitions lead to parsing errors)

The convert-smtlib option currently only works with the query_wizard. I have tested the outputs and cvc5 successfully parses them.

Let me know if you have any questions. Thanks!