changeset 67522 | 9e712280cc37 |
parent 66661 | fdab65297bd6 |
child 69205 | 8050734eee3e |
--- a/src/HOL/Tools/SMT/smt_solver.ML Sun Jan 28 16:09:00 2018 +0100 +++ b/src/HOL/Tools/SMT/smt_solver.ML Sun Jan 28 19:28:52 2018 +0100 @@ -94,7 +94,7 @@ SMT_Config.with_timeout ctxt (run ctxt name mk_cmd) input val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err - val output = fst (take_suffix (equal "") res) + val output = drop_suffix (equal "") res val _ = SMT_Config.trace_msg ctxt (pretty "Result:") output val _ = member (op =) normal_return_codes return_code orelse