Merge pull request #1361 from diffblue/property_and1-aig

Netlist engine: ignore various Verilog symbols

Author: tautschnig

regression/verilog/Makefile

@@ -7,3 +7,6 @@ test:
 
 test-z3:
 	@$(TEST_PL) -e -p -c "../../../src/ebmc/ebmc --z3" -X broken-smt-backend
+
+test-aig:
+	@$(TEST_PL) -e -p -c "../../../src/ebmc/ebmc --aig"

regression/verilog/SVA/property_and1.aig.desc

@@ -0,0 +1,9 @@
+CORE
+property_and1.sv
+--aig --bound 5
+^\[.*\] always \(main\.P1 and main\.P1\): PROVED up to bound 5$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

src/trans-netlist/trans_to_netlist.cpp

@@ -211,6 +211,18 @@ void convert_trans_to_netlistt::map_vars(
 
     if (symbol.is_property)
       return; // ignore properties
+    else if(
+      symbol.type.id() == ID_verilog_sva_sequence ||
+      symbol.type.id() == ID_verilog_sva_property)
+    {
+      return; // ignore properties
+    }
+    else if(
+      symbol.type.id() == ID_natural || symbol.type.id() == ID_integer ||
+      symbol.type.id() == ID_verilog_genvar)
+    {
+      return; // ignore
+    }
     else if(
       symbol.type.id() == ID_module || symbol.type.id() == ID_module_instance ||
       symbol.type.id() == ID_primitive_module_instance)