projects / yosys.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ab3a932) | patch
smt2, btor: Use memory_map -rom-only to make ROMs usable for k-induction
authorJannis Harder <me@jix.one>
Fri, 17 Jun 2022 15:23:13 +0000 (17:23 +0200)
committerJannis Harder <me@jix.one>
Fri, 17 Jun 2022 15:23:13 +0000 (17:23 +0200)
commit4adef63cd484d81da08ae6b5fe49b1d5d4d0b369
tree929b5c297563f8e081fc118afb0566576bbf4968tree
parentab3a9325c33b5b1b9de6971b6931ee12c3e3871ccommit | diff
smt2, btor: Use memory_map -rom-only to make ROMs usable for k-induction

This avoids provability regressions now that we infer more ROMs.

This fixes #3378
backends/btor/btor.cc diff | blob | history
backends/smt2/smt2.cc diff | blob | history