diff --git a/src/ast/card_decl_plugin.cpp b/src/ast/card_decl_plugin.cpp
index acb6d8adb..16199384b 100644
--- a/src/ast/card_decl_plugin.cpp
+++ b/src/ast/card_decl_plugin.cpp
@@ -20,7 +20,8 @@ Revision History:
 #include "card_decl_plugin.h"
 
 card_decl_plugin::card_decl_plugin():
-    m_at_most_sym("at-most")
+    m_at_most_sym("at-most"),
+    m_pble_sym("pble")
 {}
 
 func_decl * card_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
@@ -32,16 +33,36 @@ func_decl * card_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
             m.raise_exception("invalid non-Boolean sort applied to 'at-most'");
         }
     }
-    if (num_parameters != 1 || !parameters[0].is_int() || parameters[0].get_int() < 0) {
-        m.raise_exception("function 'at-most' expects one non-negative integer parameter");
+    switch(k) {
+    case OP_AT_MOST_K: {
+        if (num_parameters != 1 || !parameters[0].is_int() || parameters[0].get_int() < 0) {
+            m.raise_exception("function 'at-most' expects one non-negative integer parameter");
+        }
+        func_decl_info info(m_family_id, OP_AT_MOST_K, 1, parameters);
+        return m.mk_func_decl(m_at_most_sym, arity, domain, m.mk_bool_sort(), info);
+    }
+    case OP_PB_LE: {
+        if (num_parameters != 1 + arity || !parameters[0].is_int()) {
+            m.raise_exception("function 'pble' expects arity+1 integer parameters");
+        }
+        for (unsigned i = 1; i < num_parameters; ++i) {
+            if (!parameters[i].is_int()) {
+                m.raise_exception("function 'pble' expects arity+1 integer parameters");
+            }
+        }
+        func_decl_info info(m_family_id, OP_PB_LE, num_parameters, parameters);
+        return m.mk_func_decl(m_pble_sym, arity, domain, m.mk_bool_sort(), info);
+    }
+    default:
+        UNREACHABLE();
+        return 0;
     }
-    func_decl_info info(m_family_id, OP_AT_MOST_K, 1, parameters);
-    return m.mk_func_decl(m_at_most_sym, arity, domain, m.mk_bool_sort(), info);
 }
 
 void card_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
     if (logic == symbol::null) {
         op_names.push_back(builtin_name(m_at_most_sym.bare_str(), OP_AT_MOST_K));
+        op_names.push_back(builtin_name(m_pble_sym.bare_str(), OP_PB_LE));
     }
 }
 
@@ -65,8 +86,30 @@ bool card_util::is_at_most_k(app *a, unsigned& k) const {
     }
 }
 
-unsigned card_util::get_k(app *a) const {
-    SASSERT(is_at_most_k(a));
-    return static_cast<unsigned>(a->get_decl()->get_parameter(0).get_int());
+int card_util::get_k(app *a) const {
+    SASSERT(is_at_most_k(a) || is_le(a));
+    return a->get_decl()->get_parameter(0).get_int();
 }
 
+
+bool card_util::is_le(app *a) const {
+    return is_app_of(a, m_fid, OP_PB_LE);
+}
+
+bool card_util::is_le(app* a, int& k) const {
+    if (is_le(a)) {
+        k = get_k(a);
+        return true;
+    }
+    else {
+        return false;
+    }
+}
+
+int card_util::get_le_coeff(app* a, unsigned index) {
+    SASSERT(is_le(a));
+    SASSERT(1 + index < a->get_decl()->get_num_parameters());
+    return a->get_decl()->get_parameter(index + 1).get_int();
+}
+
+
diff --git a/src/ast/card_decl_plugin.h b/src/ast/card_decl_plugin.h
index 3529a1a04..28a22b0be 100644
--- a/src/ast/card_decl_plugin.h
+++ b/src/ast/card_decl_plugin.h
@@ -30,14 +30,17 @@ hence:
 #include"ast.h"
  
 enum card_op_kind {
-    OP_AT_MOST_K,
+    OP_AT_MOST_K,  // at most K Booleans are true.
+    OP_PB_LE,      // pseudo-Boolean <= (generalizes at_most_k)
     LAST_CARD_OP
 };
 
 
 class card_decl_plugin : public decl_plugin {
     symbol m_at_most_sym;
+    symbol m_pble_sym;
     func_decl * mk_at_most(unsigned arity, unsigned k);
+    func_decl * mk_le(unsigned arity, int const* coeffs, int k);
 public:
     card_decl_plugin();
     virtual ~card_decl_plugin() {}
@@ -54,7 +57,8 @@ public:
     //
     // Contract for func_decl:
     //   parameters[0] - integer (at most k elements)
-    //   all sorts are Booleans
+    //      all sorts are Booleans
+    //    parameters[1] .. parameters[arity] - coefficients
     virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
                                      unsigned arity, sort * const * domain, sort * range);
     virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
@@ -68,9 +72,13 @@ public:
     card_util(ast_manager& m):m(m), m_fid(m.mk_family_id("card")) {}
     ast_manager & get_manager() const { return m; }
     app * mk_at_most_k(unsigned num_args, expr * const * args, unsigned k);
+    app * mk_le(unsigned num_args, int * const* coeffs, expr * const * args, int k);
     bool is_at_most_k(app *a) const;
     bool is_at_most_k(app *a, unsigned& k) const;
-    unsigned get_k(app *a) const;
+    int  get_k(app *a) const;
+    bool is_le(app *a) const;
+    bool is_le(app* a, int& k) const;
+    int  get_le_coeff(app* a, unsigned index); 
 };