zchaff_with_proofs does not delete zChaff\s resolve_trace file anymore
authorwebertj
Wed Sep 21 22:01:09 2005 +0200 (2005-09-21)
changeset 17577e87bf1d8f17a
parent 17576 3be0d6cfbc3a
child 17578 e07af5fad73f
zchaff_with_proofs does not delete zChaff\s resolve_trace file anymore
src/HOL/Tools/sat_solver.ML
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Wed Sep 21 21:01:27 2005 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Wed Sep 21 22:01:09 2005 +0200
     1.3 @@ -511,7 +511,7 @@
     1.4  
     1.5  (* ------------------------------------------------------------------------- *)
     1.6  (* Internal SAT solver, available as 'SatSolver.invoke_solver "auto"': uses  *)
     1.7 -(* the first installed solver (other than "auto" itself) that does not raise *)
     1.8 +(* the last installed solver (other than "auto" itself) that does not raise  *)
     1.9  (* 'NOT_CONFIGURED'.  (However, the solver may return 'UNKNOWN'.)            *)
    1.10  (* ------------------------------------------------------------------------- *)
    1.11  
    1.12 @@ -564,7 +564,6 @@
    1.13  			(* string list *)
    1.14  			val proof_lines = ((split_lines o File.read) (Path.unpack "resolve_trace"))
    1.15  				handle _ => raise INVALID_PROOF "Could not read file \"resolve_trace\""
    1.16 -			val _ = try File.rm (Path.unpack "resolve_trace")
    1.17  			(* PropLogic.prop_formula -> int *)
    1.18  			fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
    1.19  			  | cnf_number_of_clauses _                          = 1