# HG changeset patch
# User webertj
# Date 1180734726 -7200
# Node ID f065f7c846fe60be1f6f6c62a59449e4b3b9fbec
# Parent  085fa3def13b1cf27bbe84296d4dba76a9cffc76
additional tracing information

diff -r 085fa3def13b -r f065f7c846fe src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Fri Jun 01 23:33:49 2007 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Fri Jun 01 23:52:06 2007 +0200
@@ -633,6 +633,8 @@
   val result = (Ts, terms)
     |> (* user-defined preprocessing of the subgoal *)
        (if do_pre then LA_Data.pre_decomp sg else Library.single)
+    |> tap (fn subgoals => trace_msg ("Preprocessing yields " ^
+         string_of_int (length subgoals) ^ " subgoal(s) total."))
     |> (* produce the internal encoding of (in-)equalities *)
        map (apsnd (map (fn t => (LA_Data.decomp sg t, LA_Data.domain_is_nat t))))
     |> (* splitting of inequalities *)
@@ -640,7 +642,11 @@
     |> maps (fn (Ts, subgoals) => map (pair Ts o map fst) subgoals)
     |> (* numbering of hypotheses, ignoring irrelevant ones *)
        map (apsnd (number_hyps 0))
-in result end;
+in
+  trace_msg ("Splitting of inequalities yields " ^
+    string_of_int (length result) ^ " subgoal(s) total.");
+  result
+end;
 
 fun add_atoms (ats : term list, ((lhs,_,_,rhs,_,_) : LA_Data.decompT, _)) : term list =
     (map fst lhs) union ((map fst rhs) union ats);