Netlist engine: ignore various Verilog symbols

The netlist engine now ignores various Verilog symbols that do not translate
into circuitry, e.g., properties, sequences.

Author: kroening

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,10 @@ 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)