diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-10-02 22:13:12 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-10-02 22:13:12 +0000 |
commit | b8a010d260c90efa5433a71dd317a03f051c2592 (patch) | |
tree | 40f716a0895d2302954b79de45893368af942723 /src/smt/smt_engine_scope.h | |
parent | 6e283659af0f95505e92a1826953509537f9d216 (diff) |
* re-enable some Z3 extended commands:
declare-const
declare-funs
declare-preds
define
simplify
* don't output --help on bad options, just invite user to try --help
* Datatypes from SMT2 parser now name the tester is-cons (e.g.)
* unknown results produce models, --check-model doesn't fail hard for
incorrect unknown models. removed the assert that kept arithmetic
from producing models if it saw nonlinear
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/smt/smt_engine_scope.h')
0 files changed, 0 insertions, 0 deletions