Add check that result matches benchmark status (#3028)
authorAndres Noetzli <andres.noetzli@gmail.com>
Tue, 4 Jun 2019 21:48:21 +0000 (14:48 -0700)
committerGitHub <noreply@github.com>
Tue, 4 Jun 2019 21:48:21 +0000 (14:48 -0700)
commit29959bec6e023f64cad0a5d43b18052f08ac94c5
tree46d059840df3e2e274981b9ee762c0ad17a2999f
parent23baea2452d765bb76bd576b4cd01dd67215d095
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.
src/smt/smt_engine.cpp
src/smt/smt_engine.h
test/regress/CMakeLists.txt
test/regress/regress0/bv/ackermann1.smt2
test/regress/regress0/bv/ackermann4.smt2
test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt
test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2
test/regress/regress0/sets/mar2014/sharing-preregister.smt2
test/regress/regress0/smtlib/set-info-status.smt2 [new file with mode: 0644]
test/regress/regress1/quantifiers/qbv-test-invert-bvcomp.smt2
test/regress/regress1/quantifiers/qe.smt2