SVA-to-Buechi: fix [+]

kroening · kroening · commit d88f6f6751c6 · 2025-06-04T17:18:32.000-07: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
@@ -473,7 +473,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
`@@ -473,7 +473,11 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)`
`473`	`473`	`else if(expr.id() == ID_sva_sequence_repetition_plus) // something[+]`
`474`	`474`	`{`
`475`	`475`	`PRECONDITION(mode == SVA_SEQUENCE);`
`476`		`- return suffix("[+]", expr, mode);`
	`476`	`+ unary_exprt new_expr{`
	`477`	`+ ID_sva_sequence_repetition_plus,`
	`478`	`+ to_sva_sequence_repetition_plus_expr(expr).op(),`
	`479`	`+ expr.type()};`
	`480`	`+ return suffix("[+]", new_expr, mode);`
`477`	`481`	`}`
`478`	`482`	`else if(expr.id() == ID_sva_sequence_goto_repetition) // something[->n]`
`479`	`483`	`{`