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

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 7de5deadd71b089d92a654dd6f7445113fdd4273..5be9bf324c33e18c96cb07e15f182a7c2062e1ea 100644 (file)
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -1402,6 +1402,7 @@ struct BtorBackend : public Backend {
                log_header(design, "Executing BTOR backend.\n");
 
                log_push();
+               Pass::call(design, "memory_map -rom-only");
                Pass::call(design, "bmuxmap");
                Pass::call(design, "demuxmap");
                log_pop();

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 7481e0510559dabfe6282f26c55aed0ca9b7ef8e..6e70f904311b72d6920f31c772fa7a7bdd686062 100644 (file)
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -1609,6 +1609,7 @@ struct Smt2Backend : public Backend {
                log_header(design, "Executing SMT2 backend.\n");
 
                log_push();
+               Pass::call(design, "memory_map -rom-only");
                Pass::call(design, "bmuxmap");
                Pass::call(design, "demuxmap");
                log_pop();