Support for bounded model checking and SSA Transformation in Chiron Framework.

[AmoghBhagwat]

Add feature to perform bounded model checking to verify properties specified by the user in the code.

[lahiri-phdworks]

Brief description feature

Provide the details of the feature, explain it's functionality.

Example

Give a test case and related commands that show the utility of the feature.

Please add a atleast 3 test cases to the repository which shows how the feature works and what are the outcomes.

# test

Why is the feature interesting?

Give use cases for the feature.

Screenshots

Please add screenshots whenever possible.

Other Details

Please add additional details that you want the developers to be aware of about the feature. Eg. good use cases (if any).

@AmoghBhagwat @debrajk22 Can you please add these details and some interesting testcases (nested loops, if-else etc)

[lahiri-phdworks]

@AmoghBhagwat @debrajk22 Can you please create a Pull Request to branch https://github.com/PRAISE-group/Chiron-Framework/tree/cs335_ssa_bmc instead of master. I am closing this PR, please create a fresh one.

[lahiri-phdworks]

@AmoghBhagwat @debrajk22 You do not have to do anything. I will review and merge accordingly. Thanks for your PR. Appreciate the work done.

[AmoghBhagwat]

@lahiri-phdworks I think you are merging into the wrong branch, our project is cs335_ssa_bmc and not cs335_smtlib_z3.