diff --git a/src/ast/pb_decl_plugin.cpp b/src/ast/pb_decl_plugin.cpp
index 16ece2d40..bfe39e3ae 100644
--- a/src/ast/pb_decl_plugin.cpp
+++ b/src/ast/pb_decl_plugin.cpp
@@ -44,7 +44,6 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
     case OP_PB_LE: sym = m_pble_sym; break;
     case OP_PB_GE: sym = m_pbge_sym; break;
     case OP_PB_EQ: sym = m_pbeq_sym; break;
-    case OP_PB_ODD: sym = symbol("is-odd"); break;
     default: break;
     }
     switch(k) {
@@ -55,15 +54,7 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
         }
         func_decl_info info(m_family_id, k, 1, parameters);
         return m.mk_func_decl(sym, arity, domain, m.mk_bool_sort(), info);
-    }
-    case OP_PB_ODD:{
-        if (num_parameters != 0) {
-            m.raise_exception("function expects no parameters");
-        }
-        func_decl_info info(m_family_id, k, 0, parameters);
-        return m.mk_func_decl(sym, arity, domain, m.mk_bool_sort(), info);
-    }
-      
+    }      
     case OP_PB_GE:
     case OP_PB_LE: 
     case OP_PB_EQ: {
@@ -106,7 +97,6 @@ void pb_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const
         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));
         op_names.push_back(builtin_name(m_pbeq_sym.bare_str(), OP_PB_EQ));
-        op_names.push_back(builtin_name("is-odd", OP_PB_ODD));
     }
 }
 
diff --git a/src/ast/pb_decl_plugin.h b/src/ast/pb_decl_plugin.h
index fdd64561b..0750dcac7 100644
--- a/src/ast/pb_decl_plugin.h
+++ b/src/ast/pb_decl_plugin.h
@@ -35,7 +35,6 @@ enum pb_op_kind {
     OP_PB_LE,      // pseudo-Boolean <= (generalizes at_most_k)
     OP_PB_GE,      // pseudo-Boolean >= 
     OP_PB_EQ,      // equality
-    OP_PB_ODD,    // parity of arguments is odd
     OP_PB_AUX_BOOL, // auxiliary internal Boolean variable.
     LAST_PB_OP
 };
@@ -96,14 +95,12 @@ public:
     app * mk_ge(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k);
     app * mk_eq(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k);
     app * mk_lt(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k);
-    app * mk_odd(unsigned num_args, expr * const * args);
     bool is_at_most_k(func_decl *a) const;
     bool is_at_most_k(expr *a) const { return is_app(a) && is_at_most_k(to_app(a)->get_decl()); }
     bool is_at_most_k(expr *a, rational& k) const;
     bool is_at_least_k(func_decl *a) const;
     bool is_at_least_k(expr *a) const { return is_app(a) && is_at_least_k(to_app(a)->get_decl()); }
     bool is_at_least_k(expr *a, rational& k) const;
-    bool is_odd(expr* a) const;
     rational get_k(func_decl *a) const;
     rational get_k(expr *a) const { return get_k(to_app(a)->get_decl()); }
     bool is_le(func_decl *a) const;