diff --git a/src/tactic/arith/pb2bv_model_converter.cpp b/src/tactic/arith/pb2bv_model_converter.cpp
index 3e17ea675..e04383fc6 100644
--- a/src/tactic/arith/pb2bv_model_converter.cpp
+++ b/src/tactic/arith/pb2bv_model_converter.cpp
@@ -21,6 +21,10 @@ Notes:
 #include"model_v2_pp.h"
 #include"pb2bv_model_converter.h"
 
+pb2bv_model_converter::pb2bv_model_converter(ast_manager & _m) : m(_m) {
+
+}
+
 pb2bv_model_converter::pb2bv_model_converter(ast_manager & _m, obj_map<func_decl, expr*> const & c2bit, bound_manager const & bm):
     m(_m) {
     obj_map<func_decl, expr*>::iterator it  = c2bit.begin();
@@ -98,5 +102,16 @@ void pb2bv_model_converter::display(std::ostream & out) {
 }
 
 model_converter * pb2bv_model_converter::translate(ast_translation & translator) {
-    NOT_IMPLEMENTED_YET();
+    ast_manager & to = translator.to();
+    pb2bv_model_converter * res = alloc(pb2bv_model_converter, to);
+    svector<func_decl_pair>::iterator it = m_c2bit.begin();
+    svector<func_decl_pair>::iterator end = m_c2bit.end();
+    for (; it != end; it++) {
+        func_decl * f1 = translator(it->first);
+        func_decl * f2 = translator(it->second);
+        res->m_c2bit.push_back(func_decl_pair(f1, f2));
+        m.inc_ref(f1);
+        m.inc_ref(f2);
+    }
+    return res;
 }
diff --git a/src/tactic/arith/pb2bv_model_converter.h b/src/tactic/arith/pb2bv_model_converter.h
index 98cb0b235..8b6256ccc 100644
--- a/src/tactic/arith/pb2bv_model_converter.h
+++ b/src/tactic/arith/pb2bv_model_converter.h
@@ -28,6 +28,7 @@ class pb2bv_model_converter : public model_converter {
     ast_manager &             m;    
     svector<func_decl_pair>   m_c2bit;
 public:
+    pb2bv_model_converter(ast_manager & _m);
     pb2bv_model_converter(ast_manager & _m, obj_map<func_decl, expr*> const & c2bit, bound_manager const & bm);
     virtual ~pb2bv_model_converter();
     virtual void operator()(model_ref & md);