better handling of veriT's 'unknown' status
authorfleury <Mathias.Fleury@mpi-inf.mpg.de>
Fri May 20 07:54:54 2016 +0200 (2016-05-20 ago)
changeset 6310271059cf60658
parent 63101 65f1d7829463
child 63103 2394b0db133f
child 63106 412140038d3c
better handling of veriT's 'unknown' status
src/HOL/Tools/SMT/smt_solver.ML
src/HOL/Tools/SMT/smt_systems.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Wed May 18 12:24:33 2016 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri May 20 07:54:54 2016 +0200
     1.3 @@ -81,8 +81,8 @@
     1.4            with_trace ctxt ("Using cached certificate from " ^
     1.5              Path.print (Cache_IO.cache_path_of certs) ^ " ...") I output))
     1.6  
     1.7 -(* Z3 returns 1 if "get-model" or "get-model" fails *)
     1.8 -val normal_return_codes = [0, 1]
     1.9 +(* Z3 returns 1 if "get-proof" or "get-model" fails. veriT returns 255. *)
    1.10 +val normal_return_codes = [0, 1, 255]
    1.11  
    1.12  fun run_solver ctxt name mk_cmd input =
    1.13    let
     2.1 --- a/src/HOL/Tools/SMT/smt_systems.ML	Wed May 18 12:24:33 2016 +0200
     2.2 +++ b/src/HOL/Tools/SMT/smt_systems.ML	Fri May 20 07:54:54 2016 +0200
     2.3 @@ -108,8 +108,7 @@
     2.4      "--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]),
     2.5    smt_options = [(":produce-proofs", "true")],
     2.6    default_max_relevant = 200 (* FUDGE *),
     2.7 -  outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat"
     2.8 -    "(error \"status is not unsat.\")"),
     2.9 +  outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown"),
    2.10    parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),
    2.11    replay = NONE }
    2.12