diff --git a/README.md b/README.md
index cf46aca8f..52b570246 100644
--- a/README.md
+++ b/README.md
@@ -213,11 +213,11 @@ See [``examples/python``](examples/python) for examples.
 * Default input format is [SMTLIB2](http://smtlib.cs.uiowa.edu)
 
 * Other native foreign function interfaces:
+ * [C++ API](https://z3prover.github.io/api/html/group__cppapi.html)
+ * [.NET API](https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html)
+ * [Java API](https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html)
+ * [Python API](https://z3prover.github.io/api/html/namespacez3py.html) (also available in [pydoc format](https://z3prover.github.io/api/html/z3.html))
   * C
-  * C++
-  * Python
-  * Java
-  * C#
   * OCaml
 
 
diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp
index fdf48a117..41bc8ec17 100644
--- a/src/tactic/fd_solver/smtfd_solver.cpp
+++ b/src/tactic/fd_solver/smtfd_solver.cpp
@@ -335,7 +335,6 @@ namespace smtfd {
                     else if (m.is_model_value(t)) {
                         int idx = a->get_parameter(0).get_int();
                         r = m_butil.mk_numeral(rational(idx), 24); 
-                        // std::cout << expr_ref(t, m) << " --> " << mk_pp(r, m) << "\n";
                     }
                     else {
                         r = fresh_var(t);                    
@@ -346,8 +345,7 @@ namespace smtfd {
                 }
                 if (is_atom(r) && !is_uninterp_const(r)) {
                     expr* rr = fresh_var(r);
-                    m_atom_defs.push_back(m.mk_implies(rr, r));
-                    m_atom_defs.push_back(m.mk_implies(r, rr));
+                    m_atom_defs.push_back(m.mk_iff(rr, r));
                     r = rr;
                 }
                 push_trail(m_abs, m_abs_trail, t, r);
@@ -1786,20 +1784,21 @@ namespace smtfd {
                   tout << *m_model.get() << "\n";
                   );
 
-            bool found_bad = false;
-            for (expr* a : subterms(core)) {
-                expr_ref val0 = (*m_model)(a);
-                expr_ref val1 = (*m_model)(abs(a));
-                if (is_ground(a) && val0 != val1 && m.get_sort(val0) == m.get_sort(val1)) {
-                    std::cout << mk_bounded_pp(a, m, 2) << " := " << val0 << " " << val1 << "\n";
-                    found_bad = true;
+            DEBUG_CODE(
+                bool found_bad = false;
+                for (expr* a : subterms(core)) {
+                    expr_ref val0 = (*m_model)(a);
+                    expr_ref val1 = (*m_model)(abs(a));
+                    if (is_ground(a) && val0 != val1 && m.get_sort(val0) == m.get_sort(val1)) {
+                        std::cout << mk_bounded_pp(a, m, 2) << " := " << val0 << " " << val1 << "\n";
+                        found_bad = true;
+                    }
                 }
-            }
-            if (found_bad) {
-                std::cout << "core: " << core << "\n";
-                std::cout << *m_model.get() << "\n";
-                exit(0);
-            }
+                if (found_bad) {
+                    std::cout << "core: " << core << "\n";
+                    std::cout << *m_model.get() << "\n";
+                    exit(0);
+                });
 
             if (!has_q) {
                 return is_decided;