Fix email address of the bugs email list and delete obsolete RELEASE-NOTES.

2 files changed, 1 insertions, 156 deletions

diff --git a/README.md b/README.md
index 153118c6b..63e91fdc5 100644
--- a/README.md
+++ b/README.md
@@ -68,7 +68,7 @@ We are always happy to hear feedback from our users:
 * if you need to report a bug with CVC4, or make a feature request, please
   visit our bugtracker at our
   [GitHub issues](https://github.com/CVC4/CVC4/issues) page or write to the
-  cvc-bugs@cs.stanford.edu mailing list.  We are very grateful for bug reports,
+  cvc4-bugs@cs.stanford.edu mailing list.  We are very grateful for bug reports,
   as they help us improve CVC4, and patches are generally reviewed and accepted
   quickly.
 
diff --git a/RELEASE-NOTES b/RELEASE-NOTES
deleted file mode 100644
index 6e8d99700..000000000
--- a/RELEASE-NOTES
+++ /dev/null
@@ -1,155 +0,0 @@
-Release Notes for CVC4 1.7, April 2019
-
-** Getting started
-
-If you run CVC4 without arguments, you will find yourself in an interactive
-CVC4 session, which expects commands in CVC4's native language (the so-called
-"presentation" language).  To use SMT-LIB, use the "--lang smt" option on the
-command line.  For stricter adherence to the standard, use "--smtlib-strict"
-(see below regarding SMT-LIB compliance).
-
-When a filename is given on the command line, the file's extension determines
-the language parser that's used (e.g., file.smt is SMT-LIB 1.2, file.smt2
-is SMT-LIB 2.6, and file.cvc is the presentation language).  To override
-this, you can use the --lang option.
-
-** Type correctness
-
-The CVC family of systems relies on Type Correctness Conditions (TCCs) when
-mixing two types that have a compatible base type.  TCCs, and the checking of
-such, are not supported by CVC4 1.7.  This is an issue when mixing integers and
-reals.  A function defined only on integers can be applied to REAL (as INT is a
-subtype of REAL), and CVC4 will not complain.  It is up to the user to ensure
-that the REAL expression must be an integer.  If the REAL expression is not
-an integer and is used where an INT is expected, CVC4 may produce strange
-results.
-
-For example:
-
-  f : INT -> INT;
-  ASSERT f(1/3) = 0;
-  ASSERT f(2/3) = 1;
-  CHECKSAT;
-  % sat
-  COUNTEREXAMPLE;
-  % f : (INT) -> INT = LAMBDA(x1:INT) : 0;
-
-This kind of problem can be identified by checking TCCs.  Though CVC4 does not
-(yet) support TCCs, CVC3 can be used to produce TCCs for this input (with the
-+dump-tcc option). The TCC can then be checked by CVC4 or another solver.
-(CVC3 can also check TCCs at the same time it creates them, with +tcc.)
-
-** Changes in CVC's Presentation Language
-
-The native language of all solvers in the CVC family, referred to as the
-"presentation language," has undergone some revisions for CVC4.  The
-most notable is that CVC4 does _not_ add counterexample assertions to
-the current assertion set after a SAT/INVALID result.  For example:
-
-  x, y : INT;
-  ASSERT x = 1 OR x = 2;
-  ASSERT y = 1 OR y = 2;
-  ASSERT x /= y;
-  CHECKSAT;
-  % sat
-  QUERY x = 1;
-  % invalid
-  QUERY x = 2;
-  % invalid
-
-Here, CVC4 responds "invalid" to the second and third queries, because
-each has a counterexample (x=2 is a counterexample to the first, and
-x=1 is a counterexample to the second).  However, CVC3 will respond
-with "valid" to one of these two, as the first query (the CHECKSAT)
-had the side-effect of locking CVC3 into one of the two cases; the
-later queries are effectively querying the counterexample that was
-found by the first.  CVC4 removes this side-effect of the CHECKSAT and
-QUERY commands.
-
-CVC4 supports rational literals (of type REAL) in decimal; CVC3 did not
-support decimals.
-
-CVC4 does not have support for predicate subtypes, although these are
-planned for future releases.
-
-** SMT-LIB compliance
-
-Every effort has been made to make CVC4 compliant with the SMT-LIB 2.6
-standard (http://smtlib.org/).  However, when parsing SMT-LIB input,
-certain default settings don't match what is stated in the official
-standard.  To make CVC4 adhere more strictly to the standard, use the
-"--smtlib-strict" command-line option.  Even with this setting, CVC4 is
-somewhat lenient; some non-conforming input may still be parsed and
-processed.
-
-** Getting statistics
-
-Statistics can be dumped on exit (both normal and abnormal exits) with
-the --stats command line option.
-
-** Time and resource limits
-
-CVC4 can be made to self-timeout after a given number of milliseconds.
-Use the --tlimit command line option to limit the entire run of
-CVC4, or use --tlimit-per to limit each individual query separately.
-Occasionally, you may encounter a problem for which --tlimit does not work very
-well.  If you suspect this might be the case, please report it as a bug.  You
-can also use "-vv" (double verbosity) to see what CVC4 is doing.
-
-Time-limited runs are not deterministic; two consecutive runs with the
-same time limit might produce different results (i.e., one may time out
-and respond with "unknown", while the other completes and provides an
-answer).  To ensure that results are reproducible, use --rlimit or
---rlimit-per.  These options take a "resource count" (presently, based on
-the number of SAT conflicts) that limits the search time.  A word of
-caution, though: there is no guarantee that runs of different versions of
-CVC4 or of different builds of CVC4 (e.g., two CVC4 binaries with different
-features enabled, or for different architectures) will interpret the resource
-count in the same manner.
-
-CVC4 does not presently have a way to limit its memory use; you may opt
-to run it from a shell after using "ulimit" to limit the size of the
-heap.
-
-** Proof support
-
-CVC4 1.7 has support for proofs when using uninterpreted functions, arrays,
-bitvectors, or their combinations, and proofs are enabled by default.
-(Run the configure script with --disable-proof to disable proofs).  Proofs
-are exported in LFSC format.
-
-** Nonlinear arithmetic
-
-CVC4 1.7 has a state-of-the-art linear arithmetic solver as well as some
-heuristic support for non-linear arithmetic.
-
-** Portfolio solving
-
-If enabled at configure-time (./configure --with-portfolio), a second
-CVC4 binary will be produced ("pcvc4").  This binary has support for
-running multiple instances of CVC4 in different threads.  Use --threads=N
-to specify the number of threads, and use --thread0="options for thread 0"
---thread1="options for thread 1", etc., to specify a configuration for the
-threads.  Lemmas are *not* shared between the threads by default; to adjust
-this, use the --filter-lemma-length=N option to share lemmas of N literals
-(or smaller).  (Some lemmas are ineligible for sharing because they include
-literals that are "local" to one thread.)
-
-Currently, the portfolio **does not work** with the theory of inductive
-datatypes. This limitation will be addressed in a future release.
-
-** Questions ??
-
-CVC4 and its predecessors have an active user base.  You might want to
-subscribe to the mailing list (http://cvc4.stanford.edu/#Technical_Support)
-and post a question there.
-
-** Reporting bugs and making feature requests
-
-CVC4 is under active development.  Should you find a bug in CVC4's
-documentation, behavior, API, or SMT-LIB compliance, or if you have
-a feature request, please let us know on our bugtracker at
-
-  https://github.com/CVC4/CVC4/issues
-
-or send an email to cvc-bugs@cs.stanford.edu.