Fix assertion in smt_engine's getValue

Minor changes to RELASE-NOTES

diff --git a/RELEASE-NOTES b/RELEASE-NOTES
index 5a6ad2cb94e38f1505c49fc928b9e6717075d75d..38d1459ad5080e0ef441f836a4b44d186eeef734 100644 (file)
--- a/RELEASE-NOTES
+++ b/RELEASE-NOTES
@@ -1,11 +1,11 @@
-Release Notes for CVC4 1.0, October 2012
+Release Notes for CVC4 1.0, December 2012
 
 ** 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"
+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
@@ -15,10 +15,16 @@ this, you can use the --lang option.
 
 ** Type correctness
 
-Type Correctness Conditions (TCCs), and the checking of such, are not
-supported by CVC4 1.0.  Thus, a function defined only on integers can be
-applied to REAL (as INT is a subtype of REAL), and CVC4 will not complain,
-but may produce strange results.  For example:
+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.0.  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;
@@ -28,9 +34,10 @@ 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).
-The TCC can be checked by CVC3 or another solver.  (CVC3 can also check
-TCCs while solving with +tcc.)
+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 be checked by CVC3 or another solver.  (CVC3 can
+also check TCCs while solving with +tcc.)
 
 ** Changes in CVC's Presentation Language
 
@@ -71,7 +78,7 @@ Every effort has been made to make CVC4 compliant with the SMT-LIB 2.0
 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" command-line option.  Even with this setting, CVC4 is
+"--smtlib-strict" command-line option.  Even with this setting, CVC4 is
 somewhat lenient; some non-conforming input may still be parsed and
 processed.
 
@@ -79,10 +86,6 @@ For the latest news on SMT-LIB compliance, please check:
 
   http://church.cims.nyu.edu/wiki/SMT-LIB_Compliance
 
-However, please note that that page may refer to a more recent version
-(and possibly an unreleased, development version) than the one you are
-looking at.
-
 ** Getting statistics
 
 Statistics can be dumped on exit (both normal and abnormal exits) with
@@ -100,7 +103,7 @@ case, you can 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 responds with "unknown", while the other completes and provides an
+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
@@ -153,6 +156,6 @@ 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
 
-  http://church.cims.nyu.edu/bugs/
+  http://cvc4.cs.nyu.edu/bugs/
 
 or send an email to cvc-bugs@cims.nyu.edu.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 25a066e4a4d9bab50905b6f179a0b27d8dff292b..b5ed599123598228ae1a6dced73771381a4f848e 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2622,7 +2622,7 @@ Expr SmtEngine::getValue(const Expr& ex) throw(ModalException, LogicException) {
   Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(n.getType()));
 
   // ensure it's a constant
-  Assert(resultNode.isConst());
+  Assert(resultNode.getKind() == kind::LAMBDA || resultNode.isConst());
 
   if(options::abstractValues() && resultNode.getType().isArray()) {
     resultNode = d_private->mkAbstractValue(resultNode);