From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 7 Nov 2012 20:34:09 +0000 (+0000)
Subject: * Type ascription bug fixed (resolves bug 432), but there are others I discovered... 
X-Git-Tag: cvc5-1.0.0~7645
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4d04a1014f058ef2dca9859389b55d87b474d270;p=cvc5.git

* Type ascription bug fixed (resolves bug 432), but there are others I discovered (still outstanding).  :-(
* 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 4fe615286..2bcd4787f 100644
--- 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 096d18f87..bcf0cd6c1 100644
--- 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 932a00185..d3bd6ad03 100755
--- 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++ ){
       Node n = considerTerms[i];
       bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n );
-      bool hadSuccess = false;
+      bool hadSuccess CVC4_UNUSED = false;
       for( int t=(isSelected ? 0 : 1); t<2; t++ ){
         if( t==0 || !n.getAttribute(NoMatchAttribute()) ){
           considerTermsMatch[t][n] = InstMatch();
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 750469088..a225339cd 100644
--- 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 2e3f1d834..27a79ff17 100644
--- 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)