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/main/main.cpp | |
| 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/main/main.cpp')
| -rw-r--r-- | src/main/main.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/main/main.cpp b/src/main/main.cpp index e3196bb4e..9fa1db7bc 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -59,8 +59,9 @@ int main(int argc, char* argv[]) { #ifdef CVC4_COMPETITION_MODE *opts[options::out] << "unknown" << endl; #endif - cerr << "CVC4 Error:" << endl << e << endl; - printUsage(opts); + cerr << "CVC4 Error:" << endl << e << endl << endl + << "Please use --help to get help on command-line options." + << endl; } catch(Exception& e) { #ifdef CVC4_COMPETITION_MODE *opts[options::out] << "unknown" << endl; |