Bugfixes in new BTOR back-end

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 2a98d1aba293651269f13ebc9bb2f0ccb699ed87..51715ff25589654187072805314ccf6c608cc1a3 100644 (file)
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -334,7 +334,7 @@ struct BtorWorker
 
                                if (nid >= 0) {
                                        int sid = get_bv_sid(width+upper-lower+1);
-                                       int nid4 = next_nid++;
+                                       nid4 = next_nid++;
                                        btorf("%d concat %d %d %d\n", nid4, sid, nid, nid3);
                                }
 
@@ -411,8 +411,9 @@ struct BtorWorker
 
                        btorf_push(stringf("output %s", log_id(wire)));
 
+                       int sid = get_bv_sid(GetSize(wire));
                        int nid = get_sig_nid(wire);
-                       btorf("%d output %d %s\n", next_nid++, nid, log_id(wire));
+                       btorf("%d output %d %d %s\n", next_nid++, sid, nid, log_id(wire));
 
                        btorf_pop(stringf("output %s", log_id(wire)));
                }