Instrument $past when generating SMV word level

This removes Verilog's $past when outputting SMV word level, which does not
have an equivalent of $past.

Author: kroening

regression/ebmc/smv-word-level/verilog5.desc

@@ -0,0 +1,9 @@
+CORE
+verilog5.sv
+--smv-word-level
+^INIT ebmc::\$past1@1 = FALSE$
+^TRANS next\(ebmc::\$past1@1\) = main\.in$
+^LTLSPEC G main\.in = \(X ebmc::\$past1@1\)$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/smv-word-level/verilog5.sv

@@ -0,0 +1,5 @@
+module main(input clk, input in);
+
+  p1: assert property (in iff s_nexttime $past(in));
+
+endmodule

src/ebmc/ebmc_parse_options.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include "ebmc_version.h"
 #include "format_hooks.h"
 #include "instrument_buechi.h"
+#include "instrument_past.h"
 #include "liveness_to_safety.h"
 #include "netlist.h"
 #include "neural_liveness.h"
@@ -234,6 +235,8 @@ int ebmc_parse_optionst::doit()
 
     if(cmdline.isset("smv-word-level"))
     {
+      // There is no $past in SMV.
+      instrument_past(transition_system, properties);
       auto filename = cmdline.value_opt("outfile").value_or("-");
       output_filet output_file{filename};
       output_smv_word_level(