Skip to content
/ bmc Public

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

License

Notifications You must be signed in to change notification settings

wert310/bmc

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

12 Commits
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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
    

About

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

Resources

License

Stars

Watchers

Forks

Languages