diff --git a/regression/ebmc/smv-netlist/always_with_range1.desc b/regression/ebmc/smv-netlist/always_with_range1.desc index 296eb319f..ab739db8d 100644 --- a/regression/ebmc/smv-netlist/always_with_range1.desc +++ b/regression/ebmc/smv-netlist/always_with_range1.desc @@ -4,7 +4,7 @@ always_with_range1.sv ^LTLSPEC node275 & X node275 & X X node275 .* ^LTLSPEC G node275$ ^LTLSPEC node275 & X node275 & X X node275 .* -^LTLSPEC G \(\!node306 \| X node337\)$ +^LTLSPEC G \(node306 -> X node337\)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/src/temporal-logic/ltl_sva_to_string.cpp b/src/temporal-logic/ltl_sva_to_string.cpp index 7e4810421..42f136708 100644 --- a/src/temporal-logic/ltl_sva_to_string.cpp +++ b/src/temporal-logic/ltl_sva_to_string.cpp @@ -91,6 +91,11 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) { return infix(" xor ", expr, mode); } + else if( + expr.id() == ID_equal && to_equal_expr(expr).lhs().type().id() == ID_bool) + { + return infix("<->", expr, mode); + } else if(expr.id() == ID_implies) { return infix("->", expr, mode); diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp index 4caaafce2..c55479ebb 100644 --- a/src/temporal-logic/normalize_property.cpp +++ b/src/temporal-logic/normalize_property.cpp @@ -15,7 +15,6 @@ Author: Daniel Kroening, dkr@amazon.com #include #include "ltl.h" -#include "nnf.h" #include "temporal_expr.h" #include "temporal_logic.h" #include "trivial_sva.h" @@ -112,8 +111,5 @@ exprt normalize_property(exprt expr) // now do recursion expr = normalize_property_rec(expr); - // NNF - expr = property_nnf(expr); - return expr; }