SVA-to-Buechi: fix [+]

kroening · kroening · commit b41f57d44b43 · 2025-06-17T11:33:24.000+09:00
This fixes the translation of the SVA [+] operator to Buechi.
diff --git a/src/temporal-logic/ltl_sva_to_string.cpp b/src/temporal-logic/ltl_sva_to_string.cpp
@@ -477,7 +477,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);
-    return suffix("[+]", expr, mode);
+    unary_exprt new_expr{
+      ID_sva_sequence_repetition_plus,
+      to_sva_sequence_repetition_plus_expr(expr).op(),
+      expr.type()};
+    return suffix("[+]", new_expr, mode);
   }
   else if(expr.id() == ID_sva_sequence_goto_repetition) // something[->n]
   {

Original file line number	Diff line number	Diff line change
`@@ -477,7 +477,11 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)`
`477`	`477`	`else if(expr.id() == ID_sva_sequence_repetition_plus) // something[+]`
`478`	`478`	`{`
`479`	`479`	`PRECONDITION(mode == SVA_SEQUENCE);`
`480`		`- return suffix("[+]", expr, mode);`
	`480`	`+ unary_exprt new_expr{`
	`481`	`+ ID_sva_sequence_repetition_plus,`
	`482`	`+ to_sva_sequence_repetition_plus_expr(expr).op(),`
	`483`	`+ expr.type()};`
	`484`	`+ return suffix("[+]", new_expr, mode);`
`481`	`485`	`}`
`482`	`486`	`else if(expr.id() == ID_sva_sequence_goto_repetition) // something[->n]`
`483`	`487`	`{`