From 1f4390c38949829a8a2d1eedc063e7a7bee60811 Mon Sep 17 00:00:00 2001
From: Daniel Larraz <daniel-larraz@users.noreply.github.com>
Date: Mon, 30 Sep 2024 16:10:01 -0500
Subject: [PATCH] Only print UF logic once (fix 465a386)

---
 src/terms/termLib.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/terms/termLib.ml b/src/terms/termLib.ml
index 84563b2ce..a294065a1 100644
--- a/src/terms/termLib.ml
+++ b/src/terms/termLib.ml
@@ -241,11 +241,11 @@ let pp_print_features ?(enforce_logic=false) fmt l =
   if not (L.mem Q l) then fprintf fmt "QF_"
   else if L.cardinal l = 1 then fprintf fmt "UF";
   if L.is_empty l then fprintf fmt "UF";
-  if L.mem A l then (
-    if (enforce_logic || Flags.Arrays.smt ()) then fprintf fmt "A"
-    else fprintf fmt "UF"
-  );
-  if L.mem UF l then fprintf fmt "UF";
+  let smt_arrays =
+    L.mem A l && (enforce_logic || Flags.Arrays.smt ())
+  in
+  if smt_arrays then fprintf fmt "A";
+  if L.mem UF l || (L.mem A l && not smt_arrays) then fprintf fmt "UF";
   if L.mem BV l then fprintf fmt "BV";
   if L.mem NA l then fprintf fmt "N"
   else if L.mem LA l || L.mem IA l || L.mem RA l then fprintf fmt "L";