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/fmf | |
| 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/fmf')
| -rw-r--r-- | test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt index bb2630b93..ab1e41360 100644 --- a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt +++ b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt @@ -1,7 +1,6 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: unsat (benchmark Isabelle -:status sat :logic AUFLIA :extrasorts ( S1 S2 S3 S4 S5 S6 S7 S8 S9 S10 S11 S12 S13 S14 S15 S16 S17 S18 S19 S20 S21 S22 S23 S24 S25 S26 S27 S28 S29 S30 S31 S32 S33 S34 S35 S36 S37) :extrafuns ( |