Merge pull request #1385 from diffblue/sva-strong-buechi

tautschnig · web-flow · commit e67715256cd4 · 2025-11-04T12:55:40.000+01:00
SVA-&gt;Buechi: enable fragment of strong sequences
diff --git a/regression/ebmc-spot/sva-buechi/cover_sequence1.bmc.desc b/regression/ebmc-spot/sva-buechi/cover_sequence1.bmc.desc
@@ -1,8 +1,8 @@
 CORE
 ../../verilog/SVA/cover_sequence1.sv
 --buechi --bound 10 --numbered-trace
-^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 4\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$
-^\[main\.p1\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 5\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$
+^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 4\): PROVED$
+^\[main\.p1\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 5\): REFUTED up to bound 10$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc-spot/sva-buechi/cover_sequence2.bmc.desc b/regression/ebmc-spot/sva-buechi/cover_sequence2.bmc.desc
@@ -1,10 +1,10 @@
 CORE
 ../../verilog/SVA/cover_sequence2.sv
 --buechi --bound 5
-^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 100\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$
-^\[main\.p1\] cover \(main\.x == 98 ##1 main\.x == 99 ##1 main\.x == 100\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$
-^\[main\.p2\] cover \(main\.x == 3 ##1 main\.x == 4 ##1 main\.x == 5\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$
-^\[main\.p3\] cover \(main\.x == 4 ##1 main\.x == 5 ##1 main\.x == 6\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$
+^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 100\): REFUTED up to bound 5$
+^\[main\.p1\] cover \(main\.x == 98 ##1 main\.x == 99 ##1 main\.x == 100\): REFUTED up to bound 5$
+^\[main\.p2\] cover \(main\.x == 3 ##1 main\.x == 4 ##1 main\.x == 5\): PROVED$
+^\[main\.p3\] cover \(main\.x == 4 ##1 main\.x == 5 ##1 main\.x == 6\): REFUTED up to bound 5$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc-spot/sva-buechi/sequence2.bmc.desc b/regression/ebmc-spot/sva-buechi/sequence2.bmc.desc
@@ -2,7 +2,7 @@ CORE
 ../../verilog/SVA/sequence2.sv
 --buechi --bound 10
 ^\[main\.p0] weak\(##\[0:\$\] main\.x == 10\): PROVED up to bound 10$
-^\[main\.p1] strong\(##\[0:\$\] main\.x == 10\): UNSUPPORTED: sva_strong not convertible to Buechi$
+^\[main\.p1] strong\(##\[0:\$\] main\.x == 10\): UNSUPPORTED: sva_cycle_delay not convertible to Buechi$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc-spot/sva-buechi/sequence3.bmc.desc b/regression/ebmc-spot/sva-buechi/sequence3.bmc.desc
@@ -1,10 +1,10 @@
 CORE
 ../../verilog/SVA/sequence3.sv
 --buechi --bound 20 --numbered-trace
-^\[main\.p0\] strong\(##\[\*\] main\.x == 6\): UNSUPPORTED: sva_strong not convertible to Buechi$
-^\[main\.p1\] strong\(##\[\*\] main\.x == 5\): UNSUPPORTED: sva_strong not convertible to Buechi$
-^\[main\.p2\] strong\(##\[\+\] main\.x == 0\): UNSUPPORTED: sva_strong not convertible to Buechi$
-^\[main\.p3\] strong\(##\[\+\] main\.x == 5\): UNSUPPORTED: sva_strong not convertible to Buechi$
+^\[main\.p0\] strong\(##\[\*\] main\.x == 6\): UNSUPPORTED: sva_cycle_delay_star not convertible to Buechi$
+^\[main\.p1\] strong\(##\[\*\] main\.x == 5\): UNSUPPORTED: sva_cycle_delay_star not convertible to Buechi$
+^\[main\.p2\] strong\(##\[\+\] main\.x == 0\): UNSUPPORTED: sva_cycle_delay_plus not convertible to Buechi$
+^\[main\.p3\] strong\(##\[\+\] main\.x == 5\): UNSUPPORTED: sva_cycle_delay_plus not convertible to Buechi$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc-spot/sva-buechi/strong1.desc b/regression/ebmc-spot/sva-buechi/strong1.desc
@@ -1,7 +1,7 @@
 CORE
 ../../verilog/SVA/strong1.sv
 --buechi --bound 4
-^\[main\.p0\] strong\(##\[0:9\] main\.x == 5\): UNSUPPORTED: sva_strong not convertible to Buechi$
+^\[main\.p0\] strong\(##\[0:9\] main\.x == 5\): UNSUPPORTED: sva_cycle_delay not convertible to Buechi$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc-spot/sva-buechi/system_verilog_assertion4.desc b/regression/ebmc-spot/sva-buechi/system_verilog_assertion4.desc
@@ -1,8 +1,8 @@
 CORE
 ../../verilog/SVA/system_verilog_assertion4.sv
 --buechi --module main --bound 10
-^\[main\.p11\] always \(main\.x == 0 \|-> \(\(##1 main\.x == 1\) and \(not \(##2 main\.x == 3\)\)\)\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$
-^EXIT=10$
+^\[main\.p11\] always \(main\.x == 0 \|-> \(\(##1 main\.x == 1\) and \(not \(##2 main\.x == 3\)\)\)\): PROVED up to bound 10$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
diff --git a/src/temporal-logic/ltl_sva_to_string.cpp b/src/temporal-logic/ltl_sva_to_string.cpp
@@ -305,42 +305,54 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
   {
     PRECONDITION(mode == PROPERTY);
     auto &sequence = to_sva_sequence_property_expr_base(expr).sequence();
-    auto op_rec = rec(sequence, SVA_SEQUENCE);
+    auto op_rec = rec(sequence, SVA_SEQUENCE_WEAK);
 
     // weak closure
     return resultt{precedencet::ATOM, '{' + op_rec.s + '}'};
   }
   else if(expr.id() == ID_sva_strong || expr.id() == ID_sva_implicit_strong)
   {
-    throw ltl_sva_to_string_unsupportedt{expr};
+    PRECONDITION(mode == PROPERTY);
+    auto &sequence = to_sva_sequence_property_expr_base(expr).sequence();
+    auto op_rec = rec(sequence, SVA_SEQUENCE_STRONG);
+
+    // we use the weak closure, and reject cases where this does not work
+    return resultt{precedencet::ATOM, '{' + op_rec.s + '}'};
   }
   else if(expr.id() == ID_sva_or)
   {
     // can be sequence or property
-    PRECONDITION(mode == PROPERTY || mode == SVA_SEQUENCE);
+    PRECONDITION(
+      mode == PROPERTY || mode == SVA_SEQUENCE_STRONG ||
+      mode == SVA_SEQUENCE_WEAK);
     return infix("|", expr, mode);
   }
   else if(expr.id() == ID_sva_and)
   {
     // can be sequence or property
-    PRECONDITION(mode == PROPERTY || mode == SVA_SEQUENCE);
+    PRECONDITION(
+      mode == PROPERTY || mode == SVA_SEQUENCE_STRONG ||
+      mode == SVA_SEQUENCE_WEAK);
     // NLM intersection
     return infix("&", expr, mode);
   }
   else if(expr.id() == ID_sva_sequence_intersect)
   {
-    PRECONDITION(mode == SVA_SEQUENCE);
+    PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK);
     return infix("&&", expr, mode);
   }
   else if(expr.id() == ID_sva_boolean)
   {
     // can be sequence or property
-    PRECONDITION(mode == PROPERTY || mode == SVA_SEQUENCE);
+    PRECONDITION(
+      mode == PROPERTY || mode == SVA_SEQUENCE_STRONG ||
+      mode == SVA_SEQUENCE_WEAK);
     return rec(to_sva_boolean_expr(expr).op(), BOOLEAN);
   }
   else if(expr.id() == ID_sva_cycle_delay)
   {
-    PRECONDITION(mode == SVA_SEQUENCE);
+    PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK);
+
     auto &delay = to_sva_cycle_delay_expr(expr);
 
     if(delay.lhs().is_nil())
@@ -349,6 +361,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
 
       if(delay.is_range()) // ##[from:to] rhs
       {
+        if(mode == SVA_SEQUENCE_STRONG)
+          throw ltl_sva_to_string_unsupportedt{expr};
+
         auto from = numeric_cast_v<mp_integer>(delay.from());
 
         if(delay.is_unbounded()) // ##[n:$] rhs
@@ -384,6 +399,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
 
       if(delay.is_range())
       {
+        if(mode == SVA_SEQUENCE_STRONG)
+          throw ltl_sva_to_string_unsupportedt{expr};
+
         auto from = numeric_cast_v<mp_integer>(delay.from());
 
         if(from == 0)
@@ -393,6 +411,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
         }
         else if(delay.is_unbounded()) // f ##[n:$] g
         {
+          if(mode == SVA_SEQUENCE_STRONG)
+            throw ltl_sva_to_string_unsupportedt{expr};
+
           return infix(
             " ; 1[*" + integer2string(from - 1) + "..] ; ", new_expr, mode);
         }
@@ -427,7 +448,11 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
   {
     // ##[*] x ---> 1[*] ; x
     // w ##[*] x ---> w : 1[*] ; x
-    PRECONDITION(mode == SVA_SEQUENCE);
+    PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK);
+
+    if(mode == SVA_SEQUENCE_STRONG)
+      throw ltl_sva_to_string_unsupportedt{expr};
+
     auto &cycle_delay_expr = to_sva_cycle_delay_star_expr(expr);
     if(cycle_delay_expr.has_lhs())
     {
@@ -448,7 +473,11 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
   {
     // ##[+] x ---> 1[+] ; x
     // w ##[+] x ---> w : 1[+] ; x
-    PRECONDITION(mode == SVA_SEQUENCE);
+    PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK);
+
+    if(mode == SVA_SEQUENCE_STRONG)
+      throw ltl_sva_to_string_unsupportedt{expr};
+
     auto &cycle_delay_expr = to_sva_cycle_delay_plus_expr(expr);
     if(cycle_delay_expr.has_lhs())
     {
@@ -477,11 +506,14 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     expr.id() ==
     ID_sva_sequence_repetition_star) // [*] or [*n] or [*x:y] or [*x:$]
   {
-    PRECONDITION(mode == SVA_SEQUENCE);
+    PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK);
     auto &repetition = to_sva_sequence_repetition_star_expr(expr);
     unary_exprt new_expr{ID_sva_sequence_repetition_star, repetition.op()};
     if(!repetition.repetitions_given())
     {
+      if(mode == SVA_SEQUENCE_STRONG)
+        throw ltl_sva_to_string_unsupportedt{expr};
+
       return suffix("[*]", new_expr, mode);
     }
     else if(repetition.is_empty_match())
@@ -504,6 +536,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     }
     else if(repetition.is_unbounded())
     {
+      if(mode == SVA_SEQUENCE_STRONG)
+        throw ltl_sva_to_string_unsupportedt{expr};
+
       auto from = numeric_cast_v<mp_integer>(repetition.from());
       return suffix("[*" + integer2string(from) + "..]", new_expr, mode);
     }
@@ -512,7 +547,11 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
   }
   else if(expr.id() == ID_sva_sequence_repetition_plus) // something[+]
   {
-    PRECONDITION(mode == SVA_SEQUENCE);
+    PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK);
+
+    if(mode == SVA_SEQUENCE_STRONG)
+      throw ltl_sva_to_string_unsupportedt{expr};
+
     auto new_expr = unary_exprt{
       ID_sva_sequence_repetition_plus,
       to_sva_sequence_repetition_plus_expr(expr).op()};
@@ -523,7 +562,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     // ltl2tgba produces the wrong anser for [->n] and [=n]
     throw ltl_sva_to_string_unsupportedt{expr};
 
-    PRECONDITION(mode == SVA_SEQUENCE);
+    PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK);
     auto &repetition = to_sva_sequence_goto_repetition_expr(expr);
     unary_exprt new_expr{ID_sva_sequence_goto_repetition, repetition.op()};
     if(repetition.is_singleton())
@@ -542,6 +581,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     }
     else if(repetition.is_unbounded())
     {
+      if(mode == SVA_SEQUENCE_STRONG)
+        throw ltl_sva_to_string_unsupportedt{expr};
+
       auto from = numeric_cast_v<mp_integer>(repetition.from());
       return suffix("[->" + integer2string(from) + "..]", new_expr, mode);
     }
@@ -554,7 +596,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     // ltl2tgba produces the wrong anser for [->n] and [=n]
     throw ltl_sva_to_string_unsupportedt{expr};
 
-    PRECONDITION(mode == SVA_SEQUENCE);
+    PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK);
     auto &repetition = to_sva_sequence_non_consecutive_repetition_expr(expr);
     unary_exprt new_expr{
       ID_sva_sequence_non_consecutive_repetition, repetition.op()};
@@ -574,6 +616,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     }
     else if(repetition.is_unbounded())
     {
+      if(mode == SVA_SEQUENCE_STRONG)
+        throw ltl_sva_to_string_unsupportedt{expr};
+
       auto from = numeric_cast_v<mp_integer>(repetition.from());
       return suffix("[=" + integer2string(from) + "..]", new_expr, mode);
     }
@@ -583,9 +628,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
   }
   else if(expr.id() == ID_sva_sequence_first_match) // first_match(...)
   {
-    PRECONDITION(mode == SVA_SEQUENCE);
+    PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK);
     auto &sequence = to_sva_sequence_first_match_expr(expr).sequence();
-    auto op_rec = rec(sequence, SVA_SEQUENCE);
+    auto op_rec = rec(sequence, mode);
     return resultt{precedencet::ATOM, "first_match(" + op_rec.s + ')'};
   }
   else if(!is_temporal_operator(expr))
diff --git a/src/temporal-logic/ltl_sva_to_string.h b/src/temporal-logic/ltl_sva_to_string.h
@@ -57,7 +57,12 @@ class ltl_sva_to_stringt
   // Spot may or may not use the same numbering in the AP header.
   numberingt<exprt, irep_hash> atoms;
 
-  using modet = enum { PROPERTY, SVA_SEQUENCE, BOOLEAN };
+  using modet = enum {
+    PROPERTY,
+    SVA_SEQUENCE_STRONG,
+    SVA_SEQUENCE_WEAK,
+    BOOLEAN
+  };
 
   resultt prefix(std::string s, const unary_exprt &, modet);
   resultt suffix(std::string s, const unary_exprt &, modet);

Original file line number	Diff line number	Diff line change
`@@ -305,42 +305,54 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)`
`305`	`305`	`{`
`306`	`306`	`PRECONDITION(mode == PROPERTY);`
`307`	`307`	`auto &sequence = to_sva_sequence_property_expr_base(expr).sequence();`
`308`		`- auto op_rec = rec(sequence, SVA_SEQUENCE);`
	`308`	`+ auto op_rec = rec(sequence, SVA_SEQUENCE_WEAK);`
`309`	`309`
`310`	`310`	`// weak closure`
`311`	`311`	`return resultt{precedencet::ATOM, '{' + op_rec.s + '}'};`
`312`	`312`	`}`
`313`	`313`	`else if(expr.id() == ID_sva_strong \|\| expr.id() == ID_sva_implicit_strong)`
`314`	`314`	`{`
`315`		`- throw ltl_sva_to_string_unsupportedt{expr};`
	`315`	`+ PRECONDITION(mode == PROPERTY);`
	`316`	`+ auto &sequence = to_sva_sequence_property_expr_base(expr).sequence();`
	`317`	`+ auto op_rec = rec(sequence, SVA_SEQUENCE_STRONG);`
	`318`	`+`
	`319`	`+ // we use the weak closure, and reject cases where this does not work`
	`320`	`+ return resultt{precedencet::ATOM, '{' + op_rec.s + '}'};`
`316`	`321`	`}`
`317`	`322`	`else if(expr.id() == ID_sva_or)`
`318`	`323`	`{`
`319`	`324`	`// can be sequence or property`
`320`		`- PRECONDITION(mode == PROPERTY \|\| mode == SVA_SEQUENCE);`
	`325`	`+ PRECONDITION(`
	`326`	`+ mode == PROPERTY \|\| mode == SVA_SEQUENCE_STRONG \|\|`
	`327`	`+ mode == SVA_SEQUENCE_WEAK);`
`321`	`328`	`return infix("\|", expr, mode);`
`322`	`329`	`}`
`323`	`330`	`else if(expr.id() == ID_sva_and)`
`324`	`331`	`{`
`325`	`332`	`// can be sequence or property`
`326`		`- PRECONDITION(mode == PROPERTY \|\| mode == SVA_SEQUENCE);`
	`333`	`+ PRECONDITION(`
	`334`	`+ mode == PROPERTY \|\| mode == SVA_SEQUENCE_STRONG \|\|`
	`335`	`+ mode == SVA_SEQUENCE_WEAK);`
`327`	`336`	`// NLM intersection`
`328`	`337`	`return infix("&", expr, mode);`
`329`	`338`	`}`
`330`	`339`	`else if(expr.id() == ID_sva_sequence_intersect)`
`331`	`340`	`{`
`332`		`- PRECONDITION(mode == SVA_SEQUENCE);`
	`341`	`+ PRECONDITION(mode == SVA_SEQUENCE_STRONG \|\| mode == SVA_SEQUENCE_WEAK);`
`333`	`342`	`return infix("&&", expr, mode);`
`334`	`343`	`}`
`335`	`344`	`else if(expr.id() == ID_sva_boolean)`
`336`	`345`	`{`
`337`	`346`	`// can be sequence or property`
`338`		`- PRECONDITION(mode == PROPERTY \|\| mode == SVA_SEQUENCE);`
	`347`	`+ PRECONDITION(`
	`348`	`+ mode == PROPERTY \|\| mode == SVA_SEQUENCE_STRONG \|\|`
	`349`	`+ mode == SVA_SEQUENCE_WEAK);`
`339`	`350`	`return rec(to_sva_boolean_expr(expr).op(), BOOLEAN);`
`340`	`351`	`}`
`341`	`352`	`else if(expr.id() == ID_sva_cycle_delay)`
`342`	`353`	`{`
`343`		`- PRECONDITION(mode == SVA_SEQUENCE);`
	`354`	`+ PRECONDITION(mode == SVA_SEQUENCE_STRONG \|\| mode == SVA_SEQUENCE_WEAK);`
	`355`	`+`
`344`	`356`	`auto &delay = to_sva_cycle_delay_expr(expr);`
`345`	`357`
`346`	`358`	`if(delay.lhs().is_nil())`
`@@ -349,6 +361,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)`
`349`	`361`
`350`	`362`	`if(delay.is_range()) // ##[from:to] rhs`
`351`	`363`	`{`
	`364`	`+ if(mode == SVA_SEQUENCE_STRONG)`
	`365`	`+ throw ltl_sva_to_string_unsupportedt{expr};`
	`366`	`+`
`352`	`367`	`auto from = numeric_cast_v<mp_integer>(delay.from());`
`353`	`368`
`354`	`369`	`if(delay.is_unbounded()) // ##[n:$] rhs`
`@@ -384,6 +399,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)`
`384`	`399`
`385`	`400`	`if(delay.is_range())`
`386`	`401`	`{`
	`402`	`+ if(mode == SVA_SEQUENCE_STRONG)`
	`403`	`+ throw ltl_sva_to_string_unsupportedt{expr};`
	`404`	`+`
`387`	`405`	`auto from = numeric_cast_v<mp_integer>(delay.from());`
`388`	`406`
`389`	`407`	`if(from == 0)`
`@@ -393,6 +411,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)`
`393`	`411`	`}`
`394`	`412`	`else if(delay.is_unbounded()) // f ##[n:$] g`
`395`	`413`	`{`
	`414`	`+ if(mode == SVA_SEQUENCE_STRONG)`
	`415`	`+ throw ltl_sva_to_string_unsupportedt{expr};`
	`416`	`+`
`396`	`417`	`return infix(`
`397`	`418`	`" ; 1[*" + integer2string(from - 1) + "..] ; ", new_expr, mode);`
`398`	`419`	`}`
`@@ -427,7 +448,11 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)`
`427`	`448`	`{`
`428`	`449`	`// ##[] x ---> 1[] ; x`
`429`	`450`	`// w ##[] x ---> w : 1[] ; x`
`430`		`- PRECONDITION(mode == SVA_SEQUENCE);`
	`451`	`+ PRECONDITION(mode == SVA_SEQUENCE_STRONG \|\| mode == SVA_SEQUENCE_WEAK);`
	`452`	`+`
	`453`	`+ if(mode == SVA_SEQUENCE_STRONG)`
	`454`	`+ throw ltl_sva_to_string_unsupportedt{expr};`
	`455`	`+`
`431`	`456`	`auto &cycle_delay_expr = to_sva_cycle_delay_star_expr(expr);`
`432`	`457`	`if(cycle_delay_expr.has_lhs())`
`433`	`458`	`{`
`@@ -448,7 +473,11 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)`
`448`	`473`	`{`
`449`	`474`	`// ##[+] x ---> 1[+] ; x`
`450`	`475`	`// w ##[+] x ---> w : 1[+] ; x`
`451`		`- PRECONDITION(mode == SVA_SEQUENCE);`
	`476`	`+ PRECONDITION(mode == SVA_SEQUENCE_STRONG \|\| mode == SVA_SEQUENCE_WEAK);`
	`477`	`+`
	`478`	`+ if(mode == SVA_SEQUENCE_STRONG)`
	`479`	`+ throw ltl_sva_to_string_unsupportedt{expr};`
	`480`	`+`
`452`	`481`	`auto &cycle_delay_expr = to_sva_cycle_delay_plus_expr(expr);`
`453`	`482`	`if(cycle_delay_expr.has_lhs())`
`454`	`483`	`{`
`@@ -477,11 +506,14 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)`
`477`	`506`	`expr.id() ==`
`478`	`507`	`ID_sva_sequence_repetition_star) // [] or [n] or [x:y] or [x:$]`
`479`	`508`	`{`
`480`		`- PRECONDITION(mode == SVA_SEQUENCE);`
	`509`	`+ PRECONDITION(mode == SVA_SEQUENCE_STRONG \|\| mode == SVA_SEQUENCE_WEAK);`
`481`	`510`	`auto &repetition = to_sva_sequence_repetition_star_expr(expr);`
`482`	`511`	`unary_exprt new_expr{ID_sva_sequence_repetition_star, repetition.op()};`
`483`	`512`	`if(!repetition.repetitions_given())`
`484`	`513`	`{`
	`514`	`+ if(mode == SVA_SEQUENCE_STRONG)`
	`515`	`+ throw ltl_sva_to_string_unsupportedt{expr};`
	`516`	`+`
`485`	`517`	`return suffix("[*]", new_expr, mode);`
`486`	`518`	`}`
`487`	`519`	`else if(repetition.is_empty_match())`
`@@ -504,6 +536,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)`
`504`	`536`	`}`
`505`	`537`	`else if(repetition.is_unbounded())`
`506`	`538`	`{`
	`539`	`+ if(mode == SVA_SEQUENCE_STRONG)`
	`540`	`+ throw ltl_sva_to_string_unsupportedt{expr};`
	`541`	`+`
`507`	`542`	`auto from = numeric_cast_v<mp_integer>(repetition.from());`
`508`	`543`	`return suffix("[*" + integer2string(from) + "..]", new_expr, mode);`
`509`	`544`	`}`
`@@ -512,7 +547,11 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)`
`512`	`547`	`}`
`513`	`548`	`else if(expr.id() == ID_sva_sequence_repetition_plus) // something[+]`
`514`	`549`	`{`
`515`		`- PRECONDITION(mode == SVA_SEQUENCE);`
	`550`	`+ PRECONDITION(mode == SVA_SEQUENCE_STRONG \|\| mode == SVA_SEQUENCE_WEAK);`
	`551`	`+`
	`552`	`+ if(mode == SVA_SEQUENCE_STRONG)`
	`553`	`+ throw ltl_sva_to_string_unsupportedt{expr};`
	`554`	`+`
`516`	`555`	`auto new_expr = unary_exprt{`
`517`	`556`	`ID_sva_sequence_repetition_plus,`
`518`	`557`	`to_sva_sequence_repetition_plus_expr(expr).op()};`
`@@ -523,7 +562,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)`
`523`	`562`	`// ltl2tgba produces the wrong anser for [->n] and [=n]`
`524`	`563`	`throw ltl_sva_to_string_unsupportedt{expr};`
`525`	`564`
`526`		`- PRECONDITION(mode == SVA_SEQUENCE);`
	`565`	`+ PRECONDITION(mode == SVA_SEQUENCE_STRONG \|\| mode == SVA_SEQUENCE_WEAK);`
`527`	`566`	`auto &repetition = to_sva_sequence_goto_repetition_expr(expr);`
`528`	`567`	`unary_exprt new_expr{ID_sva_sequence_goto_repetition, repetition.op()};`
`529`	`568`	`if(repetition.is_singleton())`
`@@ -542,6 +581,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)`
`542`	`581`	`}`
`543`	`582`	`else if(repetition.is_unbounded())`
`544`	`583`	`{`
	`584`	`+ if(mode == SVA_SEQUENCE_STRONG)`
	`585`	`+ throw ltl_sva_to_string_unsupportedt{expr};`
	`586`	`+`
`545`	`587`	`auto from = numeric_cast_v<mp_integer>(repetition.from());`
`546`	`588`	`return suffix("[->" + integer2string(from) + "..]", new_expr, mode);`
`547`	`589`	`}`
`@@ -554,7 +596,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)`
`554`	`596`	`// ltl2tgba produces the wrong anser for [->n] and [=n]`
`555`	`597`	`throw ltl_sva_to_string_unsupportedt{expr};`
`556`	`598`
`557`		`- PRECONDITION(mode == SVA_SEQUENCE);`
	`599`	`+ PRECONDITION(mode == SVA_SEQUENCE_STRONG \|\| mode == SVA_SEQUENCE_WEAK);`
`558`	`600`	`auto &repetition = to_sva_sequence_non_consecutive_repetition_expr(expr);`
`559`	`601`	`unary_exprt new_expr{`
`560`	`602`	`ID_sva_sequence_non_consecutive_repetition, repetition.op()};`
`@@ -574,6 +616,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)`
`574`	`616`	`}`
`575`	`617`	`else if(repetition.is_unbounded())`
`576`	`618`	`{`
	`619`	`+ if(mode == SVA_SEQUENCE_STRONG)`
	`620`	`+ throw ltl_sva_to_string_unsupportedt{expr};`
	`621`	`+`
`577`	`622`	`auto from = numeric_cast_v<mp_integer>(repetition.from());`
`578`	`623`	`return suffix("[=" + integer2string(from) + "..]", new_expr, mode);`
`579`	`624`	`}`
`@@ -583,9 +628,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)`
`583`	`628`	`}`
`584`	`629`	`else if(expr.id() == ID_sva_sequence_first_match) // first_match(...)`
`585`	`630`	`{`
`586`		`- PRECONDITION(mode == SVA_SEQUENCE);`
	`631`	`+ PRECONDITION(mode == SVA_SEQUENCE_STRONG \|\| mode == SVA_SEQUENCE_WEAK);`
`587`	`632`	`auto &sequence = to_sva_sequence_first_match_expr(expr).sequence();`
`588`		`- auto op_rec = rec(sequence, SVA_SEQUENCE);`
	`633`	`+ auto op_rec = rec(sequence, mode);`
`589`	`634`	`return resultt{precedencet::ATOM, "first_match(" + op_rec.s + ')'};`
`590`	`635`	`}`
`591`	`636`	`else if(!is_temporal_operator(expr))`