diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-13 00:03:35 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-11-13 00:03:35 -0600 |
| commit | 6beda739210b7bd13adbb7f62b0c4361156986ee (patch) | |
| tree | 1e86229fc763f589e22a1eab2541d87537fcea59 /src/smt/smt_engine.h | |
| parent | 5d0a5e5571044000fdaf0d908bace8ed7c1c536a (diff) | |
Distinguish unknown status for model printing (#3454)
Diffstat (limited to 'src/smt/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index d99606126..a91a3a201 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -838,8 +838,8 @@ class CVC4_PUBLIC SmtEngine typedef context::CDList<Node> NodeList; /** - * The current mode of the solver, see Figure 4.1 on page 52 of the - * SMT-LIB version 2.6 standard + * The current mode of the solver, which is an extension of Figure 4.1 on + * page 52 of the SMT-LIB version 2.6 standard * http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf */ enum SmtMode @@ -848,8 +848,10 @@ class CVC4_PUBLIC SmtEngine SMT_MODE_START, // normal state of the solver, after assert/push/pop/declare/define SMT_MODE_ASSERT, - // immediately after a check-sat returning "sat" or "unknown" + // immediately after a check-sat returning "sat" SMT_MODE_SAT, + // immediately after a check-sat returning "unknown" + SMT_MODE_SAT_UNKNOWN, // immediately after a check-sat returning "unsat" SMT_MODE_UNSAT, // immediately after a successful call to get-abduct |