Merge pull request #1098 from daniel-larraz/smt-arrays-logic

Do not add UF to logic if using smt arrays

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
 

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"