Bugfix in SMV back-end for partially unassigned wires

diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc
index 03959a4f7c3bf372a61ec1265f4c3abbc7508c97..fdf022c5aac67c3d57a034a06f56ba0adbde9229 100644 (file)
--- a/backends/smv/smv.cc
+++ b/backends/smv/smv.cc
@@ -578,15 +578,13 @@ struct SmvWorker
 
                        for (int i = 0; i < wire->width; i++)
                        {
-                               SigBit bit = sigmap(SigBit(wire, i));
-
                                if (!expr.empty())
                                        expr = " :: " + expr;
 
-                               if (partial_assignment_bits.count(bit))
+                               if (partial_assignment_bits.count(sigmap(SigBit(wire, i))))
                                {
                                        int width = 1;
-                                       const auto &bit_a = partial_assignment_bits.at(bit);
+                                       const auto &bit_a = partial_assignment_bits.at(sigmap(SigBit(wire, i)));
 
                                        while (i+1 < wire->width)
                                        {
@@ -624,6 +622,20 @@ struct SmvWorker
 
                                        expr = stringf("0ub%d_%s", GetSize(bits), bits.c_str()) + expr;
                                }
+                               else if (sigmap(SigBit(wire, i)) == SigBit(wire, i))
+                               {
+                                       int length = 1;
+
+                                       while (i+1 < wire->width) {
+                                               if (partial_assignment_bits.count(sigmap(SigBit(wire, i+1))))
+                                                       break;
+                                               if (sigmap(SigBit(wire, i+1)) != SigBit(wire, i+1))
+                                                       break;
+                                               i++, length++;
+                                       }
+
+                                       expr = stringf("0ub%d_0", length) + expr;
+                               }
                                else
                                {
                                        string bits;