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();