equal
deleted
inserted
replaced
94 |
94 |
95 val {redirected_output=res, output=err, return_code} = |
95 val {redirected_output=res, output=err, return_code} = |
96 SMT_Config.with_timeout ctxt (run ctxt name mk_cmd) input |
96 SMT_Config.with_timeout ctxt (run ctxt name mk_cmd) input |
97 val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err |
97 val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err |
98 |
98 |
99 val ls = rev (snd (chop_while (equal "") (rev res))) |
99 val ls = fst (take_suffix (equal "") res) |
100 val _ = SMT_Config.trace_msg ctxt (pretty "Result:") ls |
100 val _ = SMT_Config.trace_msg ctxt (pretty "Result:") ls |
101 |
101 |
102 val _ = return_code <> 0 andalso |
102 val _ = return_code <> 0 andalso |
103 raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code) |
103 raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code) |
104 in ls end |
104 in ls end |