More work on datatypes theory combination: fix bug in care graph, do not assign values for EQC of datatype type that contain only terms belonging to other theories, do not treat APPLY_UF as congruence operator, communicate equalities involving terms of external kind. Minor fixes for fun_def_process. Other minor changes.

1 files changed, 2 insertions, 2 deletions

diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index c30742ac5..93fd1dc6f 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -91,8 +91,8 @@ public:
       if( n[0].getKind()!=kind::CONST_RATIONAL ){
         throw TypeCheckingExceptionPrivate(n, "combined cardinality constraint must be a constant");
       }
-      if( n[0].getConst<Rational>().getNumerator().sgn()!=1 ){
-        throw TypeCheckingExceptionPrivate(n, "combined cardinality constraint must be positive");
+      if( n[0].getConst<Rational>().getNumerator().sgn()==-1 ){
+        throw TypeCheckingExceptionPrivate(n, "combined cardinality constraint must be non-negative");
       }
     }
     return nodeManager->booleanType();