/bmc

BMC-based non-linear horn clauses solver based on z3py

Primary LanguagePythonMIT LicenseMIT

bmc

Examples

  • Simple linear model

    time python3 bmc.py examples/example_transitions.smtlib -v

  • Simple nonlinear model

    time python3 bmc.py examples/example_transitions_nonlinear.smtlib -v

  • SOPQuery on the WebSpec browser model

    time python3 bmc.py examples/nonlinear_webspec_sopquery.smtlib -v