diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 29c492368..f116f6868 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -1126,6 +1126,7 @@ extern "C" {
         if (mk_c(c)->get_pb_fid() == _d->get_family_id()) {
             switch(_d->get_decl_kind()) {
             case OP_PB_LE: return Z3_OP_PB_LE;
+            case OP_PB_GE: return Z3_OP_PB_GE;
             case OP_AT_MOST_K: return Z3_OP_PB_AT_MOST;
             default: UNREACHABLE();
             }
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 57ab9a1b7..08e645684 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -880,6 +880,9 @@ typedef enum
       - Z3_OP_PB_LE: Generalized Pseudo-Boolean cardinality constraint.
               Example  2*x + 3*y <= 4
 
+      - Z3_OP_PB_GE: Generalized Pseudo-Boolean cardinality constraint.
+              Example  2*x + 3*y + 2*z >= 4
+
       - Z3_OP_UNINTERPRETED: kind used for uninterpreted symbols.
 */
 typedef enum {
@@ -1063,6 +1066,7 @@ typedef enum {
     // Pseudo Booleans
     Z3_OP_PB_AT_MOST=0x900,
     Z3_OP_PB_LE,
+    Z3_OP_PB_GE,
 
     Z3_OP_UNINTERPRETED         
 } Z3_decl_kind;
diff --git a/src/ast/pb_decl_plugin.cpp b/src/ast/pb_decl_plugin.cpp
index 0f9f479dd..4cc317df3 100644
--- a/src/ast/pb_decl_plugin.cpp
+++ b/src/ast/pb_decl_plugin.cpp
@@ -21,7 +21,8 @@ Revision History:
 
 pb_decl_plugin::pb_decl_plugin():
     m_at_most_sym("at-most"),
-    m_pble_sym("pble")
+    m_pble_sym("pble"),
+    m_pbge_sym("pbge")
 {}
 
 func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
@@ -53,6 +54,18 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
         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);
     }
+    case OP_PB_GE: {
+        if (num_parameters != 1 + arity || !parameters[0].is_int()) {
+            m.raise_exception("function 'pbge' expects arity+1 integer parameters");
+        }
+        for (unsigned i = 1; i < num_parameters; ++i) {
+            if (!parameters[i].is_int()) {
+                m.raise_exception("function 'pbge' expects arity+1 integer parameters");
+            }
+        }
+        func_decl_info info(m_family_id, OP_PB_GE, num_parameters, parameters);
+        return m.mk_func_decl(m_pbge_sym, arity, domain, m.mk_bool_sort(), info);
+    }
     default:
         UNREACHABLE();
         return 0;
@@ -63,15 +76,10 @@ void pb_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const
     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));
+        op_names.push_back(builtin_name(m_pbge_sym.bare_str(), OP_PB_GE));
     }
 }
 
-
-app * pb_util::mk_at_most_k(unsigned num_args, expr * const * args, unsigned k) {
-    parameter param(k);
-    return m.mk_app(m_fid, OP_AT_MOST_K, 1, &param, num_args, args, m.mk_bool_sort());
-}
-
 app * pb_util::mk_le(unsigned num_args, int const * coeffs, expr * const * args, int k) {
     vector<parameter> params;
     params.push_back(parameter(k));
@@ -81,6 +89,23 @@ app * pb_util::mk_le(unsigned num_args, int const * coeffs, expr * const * args,
     return m.mk_app(m_fid, OP_PB_LE, params.size(), params.c_ptr(), num_args, args, m.mk_bool_sort());
 }
 
+app * pb_util::mk_ge(unsigned num_args, int const * coeffs, expr * const * args, int k) {
+    vector<parameter> params;
+    params.push_back(parameter(k));
+    for (unsigned i = 0; i < num_args; ++i) {
+        params.push_back(parameter(coeffs[i]));
+    }
+    return m.mk_app(m_fid, OP_PB_GE, params.size(), params.c_ptr(), num_args, args, m.mk_bool_sort());
+}
+
+
+
+app * pb_util::mk_at_most_k(unsigned num_args, expr * const * args, unsigned k) {
+    parameter param(k);
+    return m.mk_app(m_fid, OP_AT_MOST_K, 1, &param, num_args, args, m.mk_bool_sort());
+}
+
+
 
 bool pb_util::is_at_most_k(app *a) const {
     return is_app_of(a, m_fid, OP_AT_MOST_K);
@@ -97,7 +122,7 @@ bool pb_util::is_at_most_k(app *a, unsigned& k) const {
 }
 
 int pb_util::get_k(app *a) const {
-    SASSERT(is_at_most_k(a) || is_le(a));
+    SASSERT(is_at_most_k(a) || is_le(a) || is_ge(a));
     return a->get_decl()->get_parameter(0).get_int();
 }
 
@@ -116,11 +141,25 @@ bool pb_util::is_le(app* a, int& k) const {
     }
 }
 
-int pb_util::get_le_coeff(app* a, unsigned index) {
+bool pb_util::is_ge(app *a) const {
+    return is_app_of(a, m_fid, OP_PB_GE);
+}
+
+bool pb_util::is_ge(app* a, int& k) const {
+    if (is_ge(a)) {
+        k = get_k(a);
+        return true;
+    }
+    else {
+        return false;
+    }
+}
+
+int pb_util::get_coeff(app* a, unsigned index) {
     if (is_at_most_k(a)) {
         return 1;
     }
-    SASSERT(is_le(a));
+    SASSERT(is_le(a) || is_ge(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/pb_decl_plugin.h b/src/ast/pb_decl_plugin.h
index 093236218..e7ab3ec25 100644
--- a/src/ast/pb_decl_plugin.h
+++ b/src/ast/pb_decl_plugin.h
@@ -32,6 +32,7 @@ hence:
 enum pb_op_kind {
     OP_AT_MOST_K,  // at most K Booleans are true.
     OP_PB_LE,      // pseudo-Boolean <= (generalizes at_most_k)
+    OP_PB_GE,      // pseudo-Boolean >= 
     LAST_PB_OP
 };
 
@@ -39,8 +40,10 @@ enum pb_op_kind {
 class pb_decl_plugin : public decl_plugin {
     symbol m_at_most_sym;
     symbol m_pble_sym;
+    symbol m_pbge_sym;
     func_decl * mk_at_most(unsigned arity, unsigned k);
     func_decl * mk_le(unsigned arity, int const* coeffs, int k);
+    func_decl * mk_ge(unsigned arity, int const* coeffs, int k);
 public:
     pb_decl_plugin();
     virtual ~pb_decl_plugin() {}
@@ -74,14 +77,19 @@ public:
     family_id get_family_id() const { return m_fid; }
     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);
+    app * mk_ge(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;
     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); 
+    bool is_ge(app* a) const;
+    bool is_ge(app* a, int& k) const;
+    int  get_coeff(app* a, unsigned index); 
 };
 
 
+
+
 #endif /* _PB_DECL_PLUGIN_H_ */
 
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index f32ae390e..f18664fbc 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -26,7 +26,7 @@ Notes:
 
 namespace smt {
 
-    bool theory_pb::s_debug_conflict = false; // true; // 
+    bool theory_pb::s_debug_conflict = true; // false; // true; // 
 
     void theory_pb::ineq::negate() {
         m_lit.neg();
@@ -243,7 +243,7 @@ namespace smt {
         context& ctx   = get_context();
         ast_manager& m = get_manager();
         unsigned num_args = atom->get_num_args();
-        SASSERT(m_util.is_at_most_k(atom) || m_util.is_le(atom));
+        SASSERT(m_util.is_at_most_k(atom) || m_util.is_le(atom) || m_util.is_ge(atom));
 
         if (ctx.b_internalized(atom)) {
             return false;
@@ -264,14 +264,16 @@ namespace smt {
         for (unsigned i = 0; i < num_args; ++i) {
             expr* arg = atom->get_arg(i);
             literal l = compile_arg(arg);
-            numeral c = m_util.get_le_coeff(atom, i);
+            numeral c = m_util.get_coeff(atom, i);
             args.push_back(std::make_pair(l, c));
         }
-        // turn W <= k into -W >= -k
-        for (unsigned i = 0; i < args.size(); ++i) {
-            args[i].second = -args[i].second;
+        if (m_util.is_at_most_k(atom) || m_util.is_le(atom)) {
+            // turn W <= k into -W >= -k
+            for (unsigned i = 0; i < args.size(); ++i) {
+                args[i].second = -args[i].second;
+            }
+            k = -k;
         }
-        k = -k;
         c->unique();
         lbool is_true = c->normalize();
 
@@ -921,7 +923,10 @@ namespace smt {
         }
         for (unsigned i = 0; i < c.size(); ++i) {
             literal l(c.lit(i));
-            out << c.coeff(i) << "*" << l;
+            if (c.coeff(i) != 1) {
+                out << c.coeff(i) << "*";
+            }
+            out << l;
             if (values) {
                 out << "@(" << ctx.get_assignment(l);
                 if (ctx.get_assignment(l) != l_undef) {
@@ -1091,7 +1096,7 @@ namespace smt {
 
         SASSERT(ctx.get_assignment(c.lit()) == l_true);
         if (ctx.get_assign_level(c.lit().var()) > ctx.get_base_level()) {
-            m_antecedents.push_back(~c.lit());
+            m_ineq_literals.push_back(c.lit());
         }
     }
 
@@ -1100,7 +1105,7 @@ namespace smt {
     //
     void theory_pb::resolve_conflict(literal conseq, ineq& c) {
         
-        TRACE("pb", tout << "RESOLVE: " << conseq << "\n"; display(verbose_stream(), c, true););
+        TRACE("pb", tout << "RESOLVE: " << conseq << "\n"; display(tout, c, true););
 
         bool_var v;
         context& ctx = get_context();
@@ -1120,7 +1125,7 @@ namespace smt {
 
         m_num_marks = 0;
         m_lemma.reset();
-        m_antecedents.reset();
+        m_ineq_literals.reset();
         process_ineq(c, null_literal, 1); // add consequent to lemma.
 
         // point into stack of assigned literals
@@ -1221,7 +1226,7 @@ namespace smt {
         IF_VERBOSE(1, display(verbose_stream() << "lemma: ", m_lemma););
 
         // TBD: 
-        // create clause m_antecedents \/ m_lemma;
+        // create clause m_literals \/ m_lemma;
         //
 #if 1
         ast_manager& m = get_manager();
@@ -1234,11 +1239,17 @@ namespace smt {
             coeffs.push_back(static_cast<int>(m_lemma.coeff(i)));
         }
         int k = static_cast<int>(m_lemma.k());
-        tmp = m_util.mk_le(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), k);
+        tmp = m_util.mk_ge(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), k);
         internalize_atom(to_app(tmp), false);
-        m_antecedents.push_back(literal(ctx.get_bool_var(tmp)));
-        justification* mjs = 0;
-        ctx.mk_clause(m_antecedents.size(), m_antecedents.c_ptr(), mjs, CLS_AUX_LEMMA, 0);
+        //m_ineq_literals.push_back(literal(ctx.get_bool_var(tmp)));
+        ctx.mark_as_relevant(tmp);
+        //justification* mjs = 0;
+        //ctx.mk_clause(m_ineq_literals.size(), m_ineq_literals.c_ptr(), mjs, CLS_AUX_LEMMA, 0);
+        literal l(ctx.get_bool_var(tmp));
+        ineq* cc = 0;
+        if (m_ineqs.find(l.var(), cc)) {
+            add_assign(*cc, m_ineq_literals, l);
+        }
 #endif
     }
 }
diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h
index ae7842db3..159b709e5 100644
--- a/src/smt/theory_pb.h
+++ b/src/smt/theory_pb.h
@@ -140,7 +140,7 @@ namespace smt {
         unsigned          m_num_marks;
         unsigned          m_conflict_lvl;
         ineq              m_lemma;
-        literal_vector    m_antecedents;
+        literal_vector    m_ineq_literals;
 
         // bool_var |-> index into m_lemma
         unsigned_vector   m_conseq_index;