normalize_property no longer generates NNF

None of the engines rely on NNF being passed to them, hence we can avoid
premature lowering by leaving the property unmodified.

Author: kroening

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$
 --

src/temporal-logic/normalize_property.cpp

@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
 #include <verilog/sva_expr.h>
 
 #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;
 }