diff --git a/scripts/release.yml b/scripts/release.yml
index 901afc575..e2125f809 100644
--- a/scripts/release.yml
+++ b/scripts/release.yml
@@ -6,7 +6,7 @@
 trigger: none
 
 variables:
-  ReleaseVersion: '4.8.12'
+  ReleaseVersion: '4.8.13'
 
 stages:
 
@@ -310,6 +310,7 @@ stages:
   jobs:
 
   - job: GitHubPublish
+    condition: eq(1,0)
     displayName: "Publish to GitHub"
     pool:
       vmImage: "windows-latest"
@@ -387,7 +388,7 @@ stages:
 
   # Enable on release:
   - job: PyPIPublish
-    condition: eq(1,1)
+    condition: eq(0,1)
     displayName: "Publish to PyPI"
     pool:
       vmImage: "ubuntu-latest"
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 049bf0ce2..f38db0d88 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -627,8 +627,9 @@ namespace arith {
         else if (use_nra_model() && lp().external_to_local(v) != lp::null_lpvar) {
             anum const& an = nl_value(v, *m_a1);
             if (a.is_int(o) && !m_nla->am().is_int(an))
-                value = a.mk_numeral(rational::zero(), a.is_int(o));             
-            //value = a.mk_numeral(m_nla->am(), nl_value(v, *m_a1), a.is_int(o));
+                value = a.mk_numeral(rational::zero(), a.is_int(o));       
+            else
+                value = a.mk_numeral(m_nla->am(), nl_value(v, *m_a1), a.is_int(o));
         }
         else if (v != euf::null_theory_var) {
             rational r = get_value(v);
diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index 21a02909e..ea5bfe274 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -131,6 +131,7 @@ namespace euf {
 
     void solver::dependencies2values(user_sort& us, deps_t& deps, model_ref& mdl) {
         for (enode* n : deps.top_sorted()) {
+            TRACE("model", tout << bpp(n->get_root()) << "\n");
             unsigned id = n->get_root_id();
             if (m_values.get(id, nullptr))
                 continue;