* Type ascription bug fixed (resolves bug 432), but there are others I discovered...

* Fix a documentation-building problem when building from tarballs (fixes distcheck build failure last night)
* Provide expected output for arith regression 'mod.01.smt2'
* Also, fix a compiler warning in inst_gen.cpp

(this commit was certified error- and warning-free by the test-and-commit script.)

diff --git a/Makefile.am b/Makefile.am
index 4fe615286f9f2c65773609dc0dfa63c29242ae11..2bcd4787fdbee933d983ff0f5dc1050484051785 100644 (file)
--- a/Makefile.am
+++ b/Makefile.am
@@ -126,9 +126,9 @@ man_MANS = \
        doc/libcvc4parser.3 \
        doc/libcvc4compat.3
 
-doc/pcvc4.1:
+doc/pcvc4.1: doc/cvc4.1
        rm -f doc/pcvc4.1
-       $(LN_S) cvc4.1 doc/pcvc4.1
+       cp -p "$<" "$@"
 
 # Can't put the first several in EXTRA_DIST because those are processed
 # *before* recursive "make dist", and these files are generated in a

diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 096d18f879210a6c4def735a9cb19b78551e3446..bcf0cd6c1a2a0b3a27402c5c5b50bd9ee87e084c 100644 (file)
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -675,7 +675,7 @@ DatatypeType DatatypeType::instantiate(const std::vector<Type>& params) const {
       ++i) {
     paramsNodes.push_back(*getTypeNode(*i));
   }
-  return DatatypeType(makeType(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE,paramsNodes)));
+  return DatatypeType(makeType(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE, paramsNodes)));
 }
 
 DatatypeType SelectorType::getDomain() const {

diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp
index 932a001853660e257bfd185f0459535298661c76..d3bd6ad0388d64f96990d8aa09b704d96248c9bf 100755 (executable)
--- a/src/theory/quantifiers/inst_gen.cpp
+++ b/src/theory/quantifiers/inst_gen.cpp
@@ -95,7 +95,7 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto
     for( size_t i=0; i<considerTerms.size(); i++ ){\r
       Node n = considerTerms[i];\r
       bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n );\r
-      bool hadSuccess = false;\r
+      bool hadSuccess CVC4_UNUSED = false;\r
       for( int t=(isSelected ? 0 : 1); t<2; t++ ){\r
         if( t==0 || !n.getAttribute(NoMatchAttribute()) ){\r
           considerTermsMatch[t][n] = InstMatch();\r

diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 750469088f5f306b09d89c0e284b15ef0de0209c..a225339cd3295ccdb09eac4b609ef334e10f9bfb 100644 (file)
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -273,7 +273,7 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
 
 DatatypeType Datatype::getDatatypeType() const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
-  CheckArgument(!d_self.isNull() && !DatatypeType(d_self).isParametric(), this);
+  CheckArgument(!d_self.isNull(), *this);
   return DatatypeType(d_self);
 }
 
@@ -559,7 +559,7 @@ Expr DatatypeConstructor::getConstructor() const {
 Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const {
   CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
   const Datatype& dt = Datatype::datatypeOf(d_constructor);
-  CheckArgument(dt.isParametric(), this, "this datatype constructor is not yet resolved");
+  CheckArgument(dt.isParametric(), this, "this datatype constructor is not parametric");
   DatatypeType dtt = dt.getDatatypeType();
   Matcher m(dtt);
   m.doMatching( TypeNode::fromType(dtt), TypeNode::fromType(returnType) );

diff --git a/test/regress/regress0/arith/mod.01.smt2 b/test/regress/regress0/arith/mod.01.smt2
index 2e3f1d83435a01ee5d18eaab3f5c733df20d190f..27a79ff17263995ea5445e487f6991a798b064a9 100644 (file)
--- a/test/regress/regress0/arith/mod.01.smt2
+++ b/test/regress/regress0/arith/mod.01.smt2
@@ -1,3 +1,5 @@
+; EXPECT: unknown
+; EXIT: 0
 (set-logic QF_NIA)
 (set-info :smt-lib-version 2.0)
 (set-info :status unknown)
@@ -7,4 +9,4 @@
 (assert (>= n 1))
 (assert (< (mod x n) n))
 
-(check-sat)
\ No newline at end of file
+(check-sat)