diff options
| author | Ramana Kumar | 2018-06-12 09:17:21 +0100 |
|---|---|---|
| committer | Ramana Kumar | 2018-06-12 09:19:09 +0100 |
| commit | 0903f6dd0b6d51fde7b9b3bd45216f02fee4bd85 (patch) | |
| tree | 973be8b8a09aa0307128df27e3789e2c031d8df9 /src/bytecode_util.ml | |
| parent | 2cfd94cc91ff21c23c5d0475e8d9b4d762797db0 (diff) | |
Prove test_raw_add theorem for init_state
It can be proved almost entirely by symbolic execution (in <15s) _if_
the right definitions are in the compset. It took a lot of interactive
stumbling about to discover that LUPDATE was missing from the standard
list compset.
Diffstat (limited to 'src/bytecode_util.ml')
0 files changed, 0 insertions, 0 deletions