Merge pull request #1010 from diffblue/netlist-smv-not-translated

SMV netlist: mark properties that were not translated

Author: kroening

src/trans-netlist/netlist.cpp

@@ -368,6 +368,14 @@ void netlistt::output_smv(std::ostream &out) const
       print_smv(out, std::get<GFpt>(property).p);
       out << '\n';
     }
+    else if(std::holds_alternative<not_translatedt>(property))
+    {
+      out << "-- " << id << '\n';
+      out << "-- not translated\n";
+      out << '\n';
+    }
+    else
+      UNREACHABLE;
   }
 }
 

src/trans-netlist/netlist.h

@@ -63,7 +63,11 @@ class netlistt:public aig_plus_constraintst
     literalt p;
   };
 
-  using propertyt = std::variant<Gpt, GFpt>;
+  struct not_translatedt
+  {
+  };
+
+  using propertyt = std::variant<Gpt, GFpt, not_translatedt>;
 
   // map from property ID to property netlist nodes
   using propertiest = std::map<irep_idt, propertyt>;

src/trans-netlist/trans_to_netlist.cpp

@@ -385,13 +385,20 @@ void convert_trans_to_netlistt::operator()(
         else
         {
           // unsupported
+          dest.properties.emplace(id, netlistt::not_translatedt{});
         }
       }
       else
       {
         // unsupported
+        dest.properties.emplace(id, netlistt::not_translatedt{});
       }
     }
+    else
+    {
+      // unsupported
+      dest.properties.emplace(id, netlistt::not_translatedt{});
+    }
   }
 
   // find the nondet nodes