diff --git a/regression/verilog/Makefile b/regression/verilog/Makefile
index 68b2eefbf..369d98c6a 100644
--- a/regression/verilog/Makefile
+++ b/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"
diff --git a/regression/verilog/SVA/property_and1.aig.desc b/regression/verilog/SVA/property_and1.aig.desc
new file mode 100644
index 000000000..76dba32b9
--- /dev/null
+++ b/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
+--
diff --git a/src/trans-netlist/trans_to_netlist.cpp b/src/trans-netlist/trans_to_netlist.cpp
index cea043f47..7a2f326d9 100644
--- a/src/trans-netlist/trans_to_netlist.cpp
+++ b/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)