Task #5466
closed
[solver] print the input constraint when solver returns ERROR/UNKNOWN verdict
Added by Sergey Smolov almost 10 years ago.
Updated almost 10 years ago.
Assignee:
Andrei Tatarnikov
Published in build:
141226
Description
If solver returns an ERROR (or UNKNOWN) verdict, it would be convenient to print not only error code, but the input constraint too.
- Priority changed from Normal to High
- Status changed from New to Resolved
- % Done changed from 0 to 100
Done in r728. Works the following way: if an error occurs (SolverResult contains errors), the source code of the generated SMT file is added to the error list as the last item.
- Status changed from Resolved to Verified
- Status changed from Verified to Closed
- Published in build set to 141226
Also available in: Atom
PDF