Skip to content

Property Directed Reachability implementation using Z3

Notifications You must be signed in to change notification settings

alex-sherman/pdr

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

8 Commits
 
 
 
 
 
 
 
 

Repository files navigation

CS704 Assignment 3: Implementing PDR

In order to run all PDR examples run:

python test_pdr.py run_all

Output will be printed to the screen as well as written to files with names corresponding to the test cases.

Individual tests can be run as well:

python test_pdr.py <test>

The two longest tests on my machines are counter_unsat and add_sub_unsat.
Both of them took around a minute to solve, but probably on faster machines will take much less time.
The time it takes them to run can be increased by increasing the width of the bit vectors.

    -Alex Sherman

About

Property Directed Reachability implementation using Z3

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages