diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index 4f4ce1db2..0e1c10744 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -113,11 +113,9 @@ namespace smt {
                 ::statistics st;
                 probe_ctx->collect_statistics(st);
                 unsigned conflicts = 0, decisions = 0, rlimit = 0;
-
-                // I can't figure out how to access the statistics fields, I only see an update method
-                // st.get_uint("conflicts", conflicts);
-                // st.get_uint("decisions", decisions);
-                // st.get_uint("rlimit count", rlimit);
+                conflicts = st.get_val("conflicts");
+                decisions = st.get_val("decisions");
+                rlimit = st.get_val("rlimit count");
                 score += conflicts + decisions + rlimit;
             }
 
diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp
index 632a7f750..a878afd08 100644
--- a/src/util/statistics.cpp
+++ b/src/util/statistics.cpp
@@ -81,6 +81,21 @@ struct str_lt {
 typedef map<char const *, unsigned, str_hash_proc, str_eq_proc> key2val;
 typedef map<char const *, double, str_hash_proc, str_eq_proc> key2dval;
 
+double statistics::get_val(char const * key) const {
+    key2val m_u;
+    key2dval m_d;
+    mk_map(m_stats, m_u);
+    mk_map(m_d_stats, m_d);
+
+    unsigned val = 0;
+    double dval = 0.0;
+    if (m_u.find(key, val))
+        return static_cast<double>(val);
+    if (m_d.find(key, dval))
+        return dval;
+    return 0.0;
+}
+
 unsigned get_max_len(ptr_buffer<char> & keys) {
     unsigned max = 0;
     for (unsigned i = 0; i < static_cast<unsigned>(keys.size()); i++) {
diff --git a/src/util/statistics.h b/src/util/statistics.h
index 32d6bac9f..1a0bfb897 100644
--- a/src/util/statistics.h
+++ b/src/util/statistics.h
@@ -40,6 +40,7 @@ public:
     char const * get_key(unsigned idx) const;
     unsigned get_uint_value(unsigned idx) const;
     double get_double_value(unsigned idx) const;
+    double get_val(char const * key) const;
 };
 
 inline std::ostream& operator<<(std::ostream& out, statistics const& st) { return st.display(out); }