src/HOL/Tools/SMT/smt_failure.ML
changeset 40538 b8482ff0bc92
parent 40515 25f266144206
child 40561 0125cbb5d3c7
     1.1 --- a/src/HOL/Tools/SMT/smt_failure.ML	Fri Nov 12 15:56:11 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_failure.ML	Fri Nov 12 17:28:43 2010 +0100
     1.3 @@ -10,6 +10,7 @@
     1.4      Counterexample of bool * term list |
     1.5      Time_Out |
     1.6      Out_Of_Memory |
     1.7 +    Solver_Crashed of int |
     1.8      Other_Failure of string
     1.9    val string_of_failure: Proof.context -> failure -> string
    1.10    exception SMT of failure
    1.11 @@ -22,6 +23,7 @@
    1.12    Counterexample of bool * term list |
    1.13    Time_Out |
    1.14    Out_Of_Memory |
    1.15 +  Solver_Crashed of int |
    1.16    Other_Failure of string
    1.17  
    1.18  fun string_of_failure ctxt (Counterexample (real, ex)) =
    1.19 @@ -36,6 +38,8 @@
    1.20        end
    1.21    | string_of_failure _ Time_Out = "Timed out"
    1.22    | string_of_failure _ Out_Of_Memory = "Ran out of memory"
    1.23 +  | string_of_failure _ (Solver_Crashed err) =
    1.24 +      "Solver crashed with error code " ^ string_of_int err
    1.25    | string_of_failure _ (Other_Failure msg) = msg
    1.26  
    1.27  exception SMT of failure