From 4cddd647d068dcc3fea6981a993eafc5e4ec45d2 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sat, 31 May 2025 18:31:51 -0700
Subject: [PATCH] SVA-to-Buechi: if

This adds support for if-expressions to the SVA-to-Buechi translation.
---
 src/temporal-logic/ltl_sva_to_string.cpp | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/temporal-logic/ltl_sva_to_string.cpp b/src/temporal-logic/ltl_sva_to_string.cpp
index 10729071..262a2e25 100644
--- a/src/temporal-logic/ltl_sva_to_string.cpp
+++ b/src/temporal-logic/ltl_sva_to_string.cpp
@@ -393,6 +393,14 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     PRECONDITION(mode == SVA_SEQUENCE);
     return suffix("[+]", expr, mode);
   }
+  else if(expr.id() == ID_if)
+  {
+    // c ? x : y  --->  (c∧x)∨(¬c∧y)
+    auto &if_expr = to_if_expr(expr);
+    auto a1 = and_exprt{if_expr.cond(), if_expr.true_case()};
+    auto a2 = and_exprt{not_exprt{if_expr.cond()}, if_expr.false_case()};
+    return rec(or_exprt{a1, a2}, mode);
+  }
   else if(!is_temporal_operator(expr))
   {
     auto number = atoms.number(expr);