From 465a38645ca9053abd35bae22c461d5302855b08 Mon Sep 17 00:00:00 2001
From: Daniel Larraz <daniel-larraz@users.noreply.github.com>
Date: Thu, 26 Sep 2024 15:47:36 -0500
Subject: [PATCH] Do not add UF to logic if using smt arrays

---
 src/induction/step.ml | 19 +++++++++++++++----
 src/terms/termLib.ml  |  6 ++++--
 2 files changed, 19 insertions(+), 6 deletions(-)

diff --git a/src/induction/step.ml b/src/induction/step.ml
index 408f34711..8729a37b1 100644
--- a/src/induction/step.ml
+++ b/src/induction/step.ml
@@ -652,11 +652,22 @@ let launch input_sys aparam trans =
   (* compression uses bitvectors/integers and uf *)
   let logic =
     match TransSys.get_logic trans with
-    | `Inferred fs when Flags.BmcKind.compress () ->
+    | (`Inferred fs) as l when Flags.BmcKind.compress () ->
       let open TermLib.FeatureSet in
-      if Compress.only_bv trans
-      then `Inferred (sup_logics [ fs; of_list [ BV; UF ] ])
-      else `Inferred (sup_logics [ fs; of_list [ IA; LA; UF ] ])
+      if Flags.Smt.solver () = `Z3_SMTLIB &&
+         mem Q fs && mem A fs && not (mem UF fs) then (
+        (* Disable compression so that adding UF is not required.
+           Z3 most often returns unknown when the logic includes:
+           quantifiers, arrays, and uninterpreted functions.
+           TODO: Implement compression with arrays for this case.
+        *)
+        Flags.BmcKind.set_compress false; l
+      )
+      else (
+        if Compress.only_bv trans
+        then `Inferred (sup_logics [ fs; of_list [ BV; UF ] ])
+        else `Inferred (sup_logics [ fs; of_list [ IA; LA; UF ] ])
+      )
     | l -> l
   in
 
diff --git a/src/terms/termLib.ml b/src/terms/termLib.ml
index 355601f60..84563b2ce 100644
--- a/src/terms/termLib.ml
+++ b/src/terms/termLib.ml
@@ -131,7 +131,6 @@ let rec logic_of_sort ty =
               
   | Array (ta, tr) ->
     union (logic_of_sort ta) (logic_of_sort tr)
-    |> add UF
     |> add A
 
 
@@ -242,7 +241,10 @@ 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 && (enforce_logic || Flags.Arrays.smt ()) then fprintf fmt "A";
+  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";
   if L.mem BV l then fprintf fmt "BV";
   if L.mem NA l then fprintf fmt "N"