From 5f2eed5347831a7a207d9be4e2bee199ef10320d Mon Sep 17 00:00:00 2001
From: Francesco Bertolaccini <francesco.bertolaccini@trailofbits.com>
Date: Mon, 29 Apr 2024 16:59:08 +0200
Subject: [PATCH] Handle `ITE` Z3 expressions

---
 lib/AST/IRToASTVisitor.cpp | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/lib/AST/IRToASTVisitor.cpp b/lib/AST/IRToASTVisitor.cpp
index f7190172..2d14717e 100755
--- a/lib/AST/IRToASTVisitor.cpp
+++ b/lib/AST/IRToASTVisitor.cpp
@@ -139,6 +139,14 @@ clang::Expr *IRToASTVisitor::ConvertExpr(z3::expr expr) {
       CopyProvenance(sub, neg, dec_ctx.use_provenance);
       return neg;
     }
+    case Z3_OP_ITE: {
+      CHECK_EQ(expr.num_args(), 3)
+          << "Conditional expressions must have three arguments";
+      auto cond{ConvertExpr(expr.arg(0))};
+      auto tt{ConvertExpr(expr.arg(1))};
+      auto ff{ConvertExpr(expr.arg(2))};
+      return ast.CreateConditional(cond, tt, ff);
+    }
     default:
       LOG(FATAL) << "Invalid z3 op " << expr.to_string();
   }