Skip to content

Commit

Permalink
Update README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
sdasgup3 authored Mar 30, 2019
1 parent d118c77 commit 2112098
Showing 1 changed file with 1 addition and 2 deletions.
3 changes: 1 addition & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -366,8 +366,7 @@ The directory structure:
#### Revision Note (Added 29 March)
1. Note that in the spec file, we need to encode the post condition that `control reaches else path (L2) && a+b overflow`. We modified the code to return 1 and 0 in the then and else branch of the 'r < a' conditional check. Now, for encoding if `control reaches else path`, we added a post condition to ensure that `RAX == 0`.
2. During artifact evalualtion of the the reviewer's find that the z3 (packaged with the VM version) is producing errneous model.
We found that it might be a bug in version 4.4.1 (https://github.com/Z3Prover/z3/issues/2212).
2. During artifact evalualtion, one of the the reviewers find that the z3 (packaged with the VM version) is producing errneous model. We found that it might be a bug in version 4.4.1 (https://github.com/Z3Prover/z3/issues/2212).
Hence, we recommend to use latest version of the tool.
Please download the latest z3 from `https://github.com/Z3Prover/z3/releases`
Expand Down

0 comments on commit 2112098

Please sign in to comment.