From 66fd4f8c231082c2266de07ba17b9a99b9ef6aab Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 10 Dec 2025 15:13:29 -0800 Subject: [PATCH] smv-netlist: convert iff This adds conversion for properties that contain Boolean iff to SMV netlists. --- regression/ebmc/smv-netlist/smv1.desc | 2 ++ regression/ebmc/smv-netlist/smv1.smv | 1 + src/trans-netlist/trans_to_netlist.cpp | 3 ++- 3 files changed, 5 insertions(+), 1 deletion(-) diff --git a/regression/ebmc/smv-netlist/smv1.desc b/regression/ebmc/smv-netlist/smv1.desc index caaa7e348..28e711724 100644 --- a/regression/ebmc/smv-netlist/smv1.desc +++ b/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$ -- diff --git a/regression/ebmc/smv-netlist/smv1.smv b/regression/ebmc/smv-netlist/smv1.smv index de6109f2e..a37930340 100644 --- a/regression/ebmc/smv-netlist/smv1.smv +++ b/regression/ebmc/smv-netlist/smv1.smv @@ -7,3 +7,4 @@ ASSIGN init(x):=FALSE; LTLSPEC G F x +CTLSPEC x <-> ! AX x diff --git a/src/trans-netlist/trans_to_netlist.cpp b/src/trans-netlist/trans_to_netlist.cpp index 48f2246b0..7e485b4d3 100644 --- a/src/trans-netlist/trans_to_netlist.cpp +++ b/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())