Improve BTOR memory encoding

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index b0c51579cc04b77cf3fbf0235ee2ccaa67e9e100..dd041bfaa77bb848df5f70f790a946fdb5e91711 100644 (file)
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -599,6 +599,7 @@ struct BtorWorker
                        SigSpec sig_wr_en = sigmap(cell->getPort("\\WR_EN"));
 
                        int data_sid = get_bv_sid(width);
+                       int bool_sid = get_bv_sid(1);
                        int sid = get_mem_sid(abits, width);
                        int nid = next_nid++;
                        int nid_head = nid;
@@ -638,7 +639,13 @@ struct BtorWorker
                                        int nid7 = next_nid++;
                                        btorf("%d write %d %d %d %d\n", nid7, sid, nid_head, wa_nid, nid6);
 
-                                       nid_head = nid7;
+                                       int nid8 = next_nid++;
+                                       btorf("%d redor %d %d\n", nid8, bool_sid, we_nid);
+
+                                       int nid9 = next_nid++;
+                                       btorf("%d ite %d %d %d %d\n", nid9, sid, nid8, nid7, nid_head);
+
+                                       nid_head = nid9;
                                }
                        }
 
@@ -977,6 +984,7 @@ struct BtorWorker
                                        SigSpec sig_wr_en = sigmap(cell->getPort("\\WR_EN"));
 
                                        int data_sid = get_bv_sid(width);
+                                       int bool_sid = get_bv_sid(1);
                                        int sid = get_mem_sid(abits, width);
                                        int nid_head = nid;
 
@@ -1008,7 +1016,13 @@ struct BtorWorker
                                                int nid7 = next_nid++;
                                                btorf("%d write %d %d %d %d\n", nid7, sid, nid_head, wa_nid, nid6);
 
-                                               nid_head = nid7;
+                                               int nid8 = next_nid++;
+                                               btorf("%d redor %d %d\n", nid8, bool_sid, we_nid);
+
+                                               int nid9 = next_nid++;
+                                               btorf("%d ite %d %d %d %d\n", nid9, sid, nid8, nid7, nid_head);
+
+                                               nid_head = nid9;
                                        }
 
                                        int nid2 = next_nid++;