equal
deleted
inserted
replaced
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 = rev (snd (chop_while (equal "") (rev 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 _ = null ls andalso 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 |
105 |
105 |
106 fun trace_assms ctxt = |
106 fun trace_assms ctxt = |
107 SMT_Config.trace_msg ctxt (Pretty.string_of o |
107 SMT_Config.trace_msg ctxt (Pretty.string_of o |