summaryrefslogtreecommitdiff
path: root/test/unit/theory/logic_info_white.h
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2019-06-04 14:48:21 -0700
committerGitHub <noreply@github.com>2019-06-04 14:48:21 -0700
commit29959bec6e023f64cad0a5d43b18052f08ac94c5 (patch)
tree46d059840df3e2e274981b9ee762c0ad17a2999f /test/unit/theory/logic_info_white.h
parent23baea2452d765bb76bd576b4cd01dd67215d095 (diff)
Add check that result matches benchmark status (#3028)
This commit adds a check to make sure that the result of a `(check-sat)` call matches the expected result set via `(set-info :status ...)`. In doing so, it also fixes an issue where CVC4 would crash if asked for the unsat core after setting the status to `unsat` but before calling `(check-sat)` (see regression for concrete example). This happened because CVC4 was storing the expected result and the computed result both in the same variable (the expected result wasn't really being used though). This commit keeps track of the expected result and the computed result in separate variables to fix that issue.
Diffstat (limited to 'test/unit/theory/logic_info_white.h')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback