Also fix write_aiger for UB

diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index 2815abda8346f0f959d56660ceae49dea6dde4a2..7c851bb91afe4faad50e20e01ec5b213ba321b80 100644 (file)
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -70,35 +70,35 @@ struct AigerWriter
 
        int bit2aig(SigBit bit)
        {
-               if (aig_map.count(bit) == 0)
-               {
-                       aig_map[bit] = -1;
-
-                       if (initstate_bits.count(bit)) {
-                               log_assert(initstate_ff > 0);
-                               aig_map[bit] = initstate_ff;
-                       } else
-                       if (not_map.count(bit)) {
-                               int a = bit2aig(not_map.at(bit)) ^ 1;
-                               aig_map[bit] = a;
-                       } else
-                       if (and_map.count(bit)) {
-                               auto args = and_map.at(bit);
-                               int a0 = bit2aig(args.first);
-                               int a1 = bit2aig(args.second);
-                               aig_map[bit] = mkgate(a0, a1);
-                       } else
-                       if (alias_map.count(bit)) {
-                               int a = bit2aig(alias_map.at(bit));
-                               aig_map[bit] = a;
-                       }
+               auto it = aig_map.find(bit);
+               if (it != aig_map.end()) {
+                       log_assert(it->second >= 0);
+                       return it->second;
+               }
 
-                       if (bit == State::Sx || bit == State::Sz)
-                               log_error("Design contains 'x' or 'z' bits. Use 'setundef' to replace those constants.\n");
+               // NB: Cannot use iterator returned from aig_map.insert()
+               //     since this function is called recursively
+
+               int a = -1;
+               if (not_map.count(bit)) {
+                       a = bit2aig(not_map.at(bit)) ^ 1;
+               } else
+               if (and_map.count(bit)) {
+                       auto args = and_map.at(bit);
+                       int a0 = bit2aig(args.first);
+                       int a1 = bit2aig(args.second);
+                       a = mkgate(a0, a1);
+               } else
+               if (alias_map.count(bit)) {
+                       a = bit2aig(alias_map.at(bit));
                }
 
-               log_assert(aig_map.at(bit) >= 0);
-               return aig_map.at(bit);
+               if (bit == State::Sx || bit == State::Sz)
+                       log_error("Design contains 'x' or 'z' bits. Use 'setundef' to replace those constants.\n");
+
+               log_assert(a >= 0);
+               aig_map[bit] = a;
+               return a;
        }
 
        AigerWriter(Module *module, bool zinit_mode, bool imode, bool omode, bool bmode) : module(module), zinit_mode(zinit_mode), sigmap(module)