diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-06-04 14:48:21 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-06-04 14:48:21 -0700 |
| commit | 29959bec6e023f64cad0a5d43b18052f08ac94c5 (patch) | |
| tree | 46d059840df3e2e274981b9ee762c0ad17a2999f /test/regress/regress0/bv | |
| parent | 23baea2452d765bb76bd576b4cd01dd67215d095 (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/regress/regress0/bv')
| -rw-r--r-- | test/regress/regress0/bv/ackermann1.smt2 | 1 | ||||
| -rw-r--r-- | test/regress/regress0/bv/ackermann4.smt2 | 1 |
2 files changed, 0 insertions, 2 deletions
diff --git a/test/regress/regress0/bv/ackermann1.smt2 b/test/regress/regress0/bv/ackermann1.smt2 index 218fd746b..7fd76c8cc 100644 --- a/test/regress/regress0/bv/ackermann1.smt2 +++ b/test/regress/regress0/bv/ackermann1.smt2 @@ -3,7 +3,6 @@ (set-logic QF_UFBV) (set-info :smt-lib-version 2.0) (set-info :category "crafted") -(set-info :status unsat) (declare-fun v0 () (_ BitVec 4)) (declare-fun f ((_ BitVec 4)) (_ BitVec 4)) (declare-fun g ((_ BitVec 4)) (_ BitVec 4)) diff --git a/test/regress/regress0/bv/ackermann4.smt2 b/test/regress/regress0/bv/ackermann4.smt2 index cb8ad2e55..0c1e323d5 100644 --- a/test/regress/regress0/bv/ackermann4.smt2 +++ b/test/regress/regress0/bv/ackermann4.smt2 @@ -3,7 +3,6 @@ (set-logic QF_UFBV) (set-info :smt-lib-version 2.0) (set-info :category "crafted") -(set-info :status unsat) (declare-fun v0 () (_ BitVec 4)) (declare-fun f ((_ BitVec 4)) (_ BitVec 4)) (declare-fun g ((_ BitVec 4)) (_ BitVec 4)) |