From 4adef63cd484d81da08ae6b5fe49b1d5d4d0b369 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Fri, 17 Jun 2022 17:23:13 +0200
Subject: [PATCH] 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 | 1 +
 backends/smt2/smt2.cc | 1 +
 2 files changed, 2 insertions(+)

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 7de5deadd..5be9bf324 100644
--- 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 7481e0510..6e70f9043 100644
--- 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();
-- 
2.30.2