Merge pull request #1475 from diffblue/smv-netlist-iff

smv-netlist: convert iff

Author: tautschnig

regression/ebmc/smv-netlist/smv1.desc

@@ -5,6 +5,8 @@ smv1.smv
 ^VAR smv\.main\.var\.x: boolean;$
 ^ASSIGN next\(smv\.main\.var\.x\):=\!smv\.main\.var\.x;$
 ^INIT !smv\.main\.var\.x$
+^LTLSPEC G F smv\.main\.var\.x$
+^CTLSPEC smv\.main\.var\.x <-> \!AX smv\.main\.var\.x$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/ebmc/smv-netlist/smv1.smv

@@ -7,3 +7,4 @@ ASSIGN init(x):=FALSE;
 
 LTLSPEC G F x
 
+CTLSPEC x <-> ! AX x

src/trans-netlist/trans_to_netlist.cpp

@@ -444,7 +444,8 @@ convert_trans_to_netlistt::convert_property(const exprt &expr)
   }
   else if(
     expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_not ||
-    expr.id() == ID_implies || expr.id() == ID_xor || expr.id() == ID_xnor)
+    expr.id() == ID_implies || expr.id() == ID_xor || expr.id() == ID_xnor ||
+    (expr.id() == ID_equal && to_equal_expr(expr).lhs().type().id() == ID_bool))
   {
     exprt copy = expr;
     for(auto &op : copy.operands())