--- 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) =