summaryrefslogtreecommitdiff
path: root/src/main
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2017-10-10 15:36:09 -0700
committerGitHub <noreply@github.com>2017-10-10 15:36:09 -0700
commitdd979fcdb5a952462e4d6702999b5354de5a7be8 (patch)
treecb4d590f0cba3ec2408633d7e2c70808167b2ad2 /src/main
parentb7d0c09bd12b9d0f46deab199714ce3441206d7f (diff)
Add copyright information. (#1201)
This adds option --copyright which displays copyright information for CVC4. It further extends --show-config with copyright information and adds a banner with copyright information in interactive mode.
Diffstat (limited to 'src/main')
-rw-r--r--src/main/driver_unified.cpp3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index cad662d90..8ffb47e40 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -304,7 +304,8 @@ int runCvc4(int argc, char* argv[], Options& opts) {
Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
<< " assertions:"
<< (Configuration::isAssertionBuild() ? "on" : "off")
- << endl;
+ << endl << endl;
+ Message() << Configuration::copyright() << endl;
}
if(replayParser) {
// have the replay parser use the declarations input interactively
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback