diff options
| author | Jannis Harder <me@jix.one> | 2022-10-20 13:44:45 +0200 |
|---|---|---|
| committer | Jannis Harder <me@jix.one> | 2022-10-20 13:49:47 +0200 |
| commit | 96029400cbf661fb5303572923df3f0dc17164ee (patch) | |
| tree | e4cd774dbc532aa6968e13818cc692806d2f7385 /README.md | |
| parent | 6781746872087d8c1eb3f5560fe338a693a40d7c (diff) | |
| download | yosys-96029400cbf661fb5303572923df3f0dc17164ee.tar.gz yosys-96029400cbf661fb5303572923df3f0dc17164ee.tar.bz2 yosys-96029400cbf661fb5303572923df3f0dc17164ee.zip | |
smtbmc: Do not assume skipped assertions when loading a witness trace
This is not valid when the prefix of a trace already violates
assertions. This can happen when the trace generating solver doesn't
look for a minimal length counterexample.
Diffstat (limited to 'README.md')
0 files changed, 0 insertions, 0 deletions