# HG changeset patch
# User wenzelm
# Date 1140035699 -3600
# Node ID 2103a8e14eaa4b0bae0ac0bef634a83d1a555378
# Parent  2b875dd5eb4c38ec53e8029a3a05884608185b00
counter example: avoid vacuous trace;

diff -r 2b875dd5eb4c -r 2103a8e14eaa src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Wed Feb 15 21:34:59 2006 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Feb 15 21:34:59 2006 +0100
@@ -532,12 +532,11 @@
               else IntInf.toString p ^ "/" ^ IntInf.toString q
   in a ^ " = " ^ s end;
 
-fun print_ex sds =
+fun produce_ex sds =
   curry (op ~~) sds
   #> map print_atom
   #> commas
-  #> curry (op ^) "Counter example:\n"
-  #> tracing;
+  #> curry (op ^) "Counter example:\n";
 
 fun trace_ex(sg,params,atoms,discr,n,hist:history) =
   if null hist then ()
@@ -546,9 +545,12 @@
            val (v,lineqs) :: hist' = hist
            val start = if v = ~1 then (findex0 discr n lineqs,hist')
                        else (replicate n Rat.zero,hist)
-       in warning "arith failed - see trace for a counter example";
-          print_ex ((map s_of_t atoms)~~discr) (findex discr start)
-          handle NoEx => (tracing "Sorry, no counter example.")
+           val ex = SOME (produce_ex ((map s_of_t atoms)~~discr) (findex discr start))
+             handle NoEx => NONE;
+       in
+         (case ex of
+           SOME s => (warning "arith failed - see trace for a counter example"; tracing s)
+         | NONE => warning "arith failed")
        end;
 
 fun mknat pTs ixs (atom,i) =