Do not display 0 candidates messages

As we load by default prelude with plenty of axioms, we got a lot of
messages about these axioms in the debugging printers of `Matching`.
This commit changes this behavior. We only print messages if there is at
least one candidate.

src/lib/reasoners/adt.ml

@@ -38,7 +38,7 @@ type 'a abstract =
       c_ty : Ty.t;
       c_args : (DE.term_cst * 'a) list
     }
-  (* [Cons { c_name; c_ty; c_args }] reprensents the application of the
+  (* [Cons { c_name; c_ty; c_args }] represents the application of the
      constructor [c_name] of the ADT [ty] with the arguments [c_args]. *)
 
   | Select of { d_name : DE.term_cst ; d_ty : Ty.t ; d_arg : 'a }

src/lib/reasoners/matching.ml

@@ -165,20 +165,22 @@ module Make (X : Arg) : S with type theory = X.t = struct
 
     let candidate_substitutions pat_info res =
       let open Matching_types in
-      if Options.get_debug_matching () >= 1 then
-        print_dbg
-          ~module_name:"Matching" ~function_name:"candidate_substitutions"
-          "@[<v 2>%3d candidate substitutions for Axiom %a with trigger %a@ "
-          (List.length res)
-          E.print pat_info.trigger_orig
-          E.print_list pat_info.trigger.E.content;
-      if Options.get_debug_matching() >= 2 then
-        List.iter
-          (fun gsbt ->
-             print_dbg ~header:false
-               ">>> sbs = %a  and  sbty = %a@ "
-               (SubstE.pp E.print) gsbt.sbs Ty.print_subst gsbt.sty
-          )res
+      if not @@ Compat.List.is_empty res then begin
+        if Options.get_debug_matching () >= 1 then
+          print_dbg
+            ~module_name:"Matching" ~function_name:"candidate_substitutions"
+            "@[<v 2>%3d candidate substitutions for Axiom %a with trigger %a@ "
+            (List.length res)
+            E.print pat_info.trigger_orig
+            E.print_list pat_info.trigger.E.content;
+        if Options.get_debug_matching() >= 2 then
+          List.iter
+            (fun gsbt ->
+               print_dbg ~header:false
+                 ">>> sbs = %a  and  sbty = %a@ "
+                 (SubstE.pp E.print) gsbt.sbs Ty.print_subst gsbt.sty
+            )res
+      end
 
   end
   (*BISECT-IGNORE-END*)

test.smt2

@@ -0,0 +1,10 @@
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-datatype t ((B (i Int))))
+
+(declare-const e t)
+
+(assert ((_ is B) e))
+(assert (forall ((n Int)) (distinct e (B n))))
+(check-sat)
+(get-model)