diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-10-08 23:12:28 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-10-08 23:12:28 +0000 |
| commit | e63abd23b45a078a42cafb277a4817abb4d044a1 (patch) | |
| tree | 43b8aaccc9b49887280e0c77471c5346eb1cf9c4 /src/util/configuration_private.h | |
| parent | fccdb4cbe2cde7c34e82f33e9de850a046fef888 (diff) | |
* (define-fun...) now has proper type checking in non-debug builds
(resolves bug #212)
* also closed some other type checking loopholes in SmtEngine
* small fixes to define-sort (resolves bug #214)
* infrastructural support for printing expressions in languages
other than the internal representation language using an IO
manipulator, e.g.:
cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << expr;
main() sets the output language for all streams to correspond to
the input language
* support delaying type checking in debug builds, so that one can debug
the type checker itself (before it was difficult, because debug builds did
all the type checking on Node creation!): new command-line flag
--no-early-type-checking (only makes sense for debug builds)
* disallowed copy-construction of ExprManager and NodeManager, and made other
constructors explicit; previously it was easy to unintentionally create
duplicate managers, with really weird results (i.e., disappearing
attributes!)
Diffstat (limited to 'src/util/configuration_private.h')
| -rw-r--r-- | src/util/configuration_private.h | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h index e59eacf4d..d04efe0aa 100644 --- a/src/util/configuration_private.h +++ b/src/util/configuration_private.h @@ -85,7 +85,7 @@ namespace CVC4 { #endif /* TLS */ #define CVC4_ABOUT_STRING string("\ -This is a pre-release of CVC4.\n\ +This is CVC4 version " CVC4_RELEASE_STRING "\n\n\ Copyright (C) 2009, 2010\n\ The ACSys Group\n\ Courant Institute of Mathematical Sciences\n\ @@ -99,7 +99,8 @@ this CVC4 library cannot be used in proprietary applications. Please\n\ consult the CVC4 documentation for instructions about building a version\n\ of CVC4 that links against GMP, and can be used in such applications.\n" : \ "This CVC4 library uses GMP as its multi-precision arithmetic library.\n\n\ -CVC4 is open-source and is covered by the BSD license (modified).\n") +CVC4 is open-source and is covered by the BSD license (modified).\n\n\ +THIS SOFTWARE PROVIDED AS-IS, WITHOUT ANY WARRANTIES. USE IT AT YOUR OWN RISK.\n") }/* CVC4 namespace */ |