SVA->Buechi: fix translation of ##[*] and ##[+]

This fixes the translation of the SVA operators ##[*] and ##[+] to Spot's
input language.

Author: kroening

regression/ebmc-spot/sva-buechi/cycle_delay_star1.bdd.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 ../../verilog/SVA/cycle_delay_star1.sv
 --buechi --bdd
 ^\[main.p0\] ##\[\*\] main\.x == 2 ##1 main\.x == 3: PROVED$
@@ -7,4 +7,3 @@ KNOWNBUG
 --
 ^warning: ignoring
 --
-This gives the wrong answer.

regression/ebmc-spot/sva-buechi/cycle_delay_star1.bmc.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 ../../verilog/SVA/cycle_delay_star1.sv
 --buechi --bound 10
 ^\[main.p0\] ##\[\*\] main\.x == 2 ##1 main\.x == 3: PROVED up to bound 10$
@@ -7,4 +7,3 @@ KNOWNBUG
 --
 ^warning: ignoring
 --
-This gives the wrong answer.

regression/ebmc-spot/sva-buechi/cycle_delay_star3.bdd.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 ../../verilog/SVA/cycle_delay_star3.sv
 --buechi --bdd
 ^\[main.p0\] ##\[\*\] main\.x == 4: PROVED up to bound 10$
@@ -7,4 +7,3 @@ KNOWNBUG
 --
 ^warning: ignoring
 --
-We get the wrong answer.

regression/ebmc-spot/sva-buechi/cycle_delay_star3.bmc.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 ../../verilog/SVA/cycle_delay_star3.sv
 --buechi --bound 10
 ^\[main.p0\] ##\[\*\] main\.x == 4: PROVED up to bound 10$
@@ -7,4 +7,3 @@ KNOWNBUG
 --
 ^warning: ignoring
 --
-We get the wrong answer.

src/temporal-logic/ltl_sva_to_string.cpp

@@ -423,17 +423,19 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
   }
   else if(expr.id() == ID_sva_cycle_delay_star) // ##[*] something
   {
+    // ##[*] x ---> 1[*] ; x
     PRECONDITION(mode == SVA_SEQUENCE);
     auto new_expr = unary_exprt{
       ID_sva_cycle_delay_star, to_sva_cycle_delay_star_expr(expr).rhs()};
-    return suffix("[*]", new_expr, mode);
+    return prefix("1[*] ; ", new_expr, mode);
   }
   else if(expr.id() == ID_sva_cycle_delay_plus) // ##[+] something
   {
+    // ##[+] x ---> 1[+] ; x
     PRECONDITION(mode == SVA_SEQUENCE);
     auto new_expr = unary_exprt{
-      ID_sva_cycle_delay_star, to_sva_cycle_delay_plus_expr(expr).rhs()};
-    return suffix("[+]", new_expr, mode);
+      ID_sva_cycle_delay_plus, to_sva_cycle_delay_plus_expr(expr).rhs()};
+    return prefix("1[+] ; ", new_expr, mode);
   }
   else if(expr.id() == ID_if)
   {