equal
deleted
inserted
replaced
152 () |
152 () |
153 val birth = Timer.checkRealTimer timer |
153 val birth = Timer.checkRealTimer timer |
154 val _ = if debug then Output.urgent_message "Invoking SMT solver..." else () |
154 val _ = if debug then Output.urgent_message "Invoking SMT solver..." else () |
155 |
155 |
156 val (outcome, used_facts) = |
156 val (outcome, used_facts) = |
157 SMT2_Solver.smt2_filter_preprocess ctxt [] goal weighted_facts i |
157 SMT2_Solver.smt2_filter ctxt [] goal weighted_facts i slice_timeout |
158 |> SMT2_Solver.smt2_filter_apply slice_timeout |
|
159 |> (fn {outcome, used_facts} => (outcome, used_facts)) |
158 |> (fn {outcome, used_facts} => (outcome, used_facts)) |
160 handle exn => |
159 handle exn => |
161 if Exn.is_interrupt exn then reraise exn |
160 if Exn.is_interrupt exn then reraise exn |
162 else (ML_Compiler.exn_message exn |> SMT2_Failure.Other_Failure |> SOME, []) |
161 else (ML_Compiler.exn_message exn |> SMT2_Failure.Other_Failure |> SOME, []) |
163 |
162 |