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 /RELEASE-NOTES | |
| 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 'RELEASE-NOTES')
| -rw-r--r-- | RELEASE-NOTES | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/RELEASE-NOTES b/RELEASE-NOTES index 9eadf916a..9ad246a9c 100644 --- a/RELEASE-NOTES +++ b/RELEASE-NOTES @@ -28,8 +28,9 @@ but may produce strange results. For example: COUNTEREXAMPLE; % f : (INT) -> INT = LAMBDA(x1:INT) : 0; -CVC3 can be used to produce TCCs for this input (with the +dump-tcc option), -and the TCC can be checked with CVC4. +CVC3 can be used to produce TCCs for this input (with the +dump-tcc option). +The TCC can be checked by CVC3 or another solver. (CVC3 can also check +TCCs while solving with +tcc.) ** Changes in CVC's Presentation Language @@ -75,7 +76,8 @@ processed. ** Getting statistics -Statistics can be dumped on exit (both normal and abnormal exits) +Statistics can be dumped on exit (both normal and abnormal exits) with +the --statistics command line option. ** Time and resource limits |