# HG changeset patch
# User webertj
# Date 1127332869 -7200
# Node ID e87bf1d8f17add22aa311605a41e646604e5e07b
# Parent  3be0d6cfbc3a080473ac493b7db5f93dba998e12
zchaff_with_proofs does not delete zChaff\s resolve_trace file anymore

diff -r 3be0d6cfbc3a -r e87bf1d8f17a src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Wed Sep 21 21:01:27 2005 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Wed Sep 21 22:01:09 2005 +0200
@@ -511,7 +511,7 @@
 
 (* ------------------------------------------------------------------------- *)
 (* Internal SAT solver, available as 'SatSolver.invoke_solver "auto"': uses  *)
-(* the first installed solver (other than "auto" itself) that does not raise *)
+(* the last installed solver (other than "auto" itself) that does not raise  *)
 (* 'NOT_CONFIGURED'.  (However, the solver may return 'UNKNOWN'.)            *)
 (* ------------------------------------------------------------------------- *)
 
@@ -564,7 +564,6 @@
 			(* string list *)
 			val proof_lines = ((split_lines o File.read) (Path.unpack "resolve_trace"))
 				handle _ => raise INVALID_PROOF "Could not read file \"resolve_trace\""
-			val _ = try File.rm (Path.unpack "resolve_trace")
 			(* PropLogic.prop_formula -> int *)
 			fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
 			  | cnf_number_of_clauses _                          = 1