From c826b64e35135f85f7bcde5b72f9174dce74c7c1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 16 Nov 2021 09:41:25 -0800
Subject: [PATCH] prepare release

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/release.yml          | 5 +++--
 src/sat/smt/arith_solver.cpp | 5 +++--
 src/sat/smt/euf_model.cpp    | 1 +
 3 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/scripts/release.yml b/scripts/release.yml
index 901afc57562..e2125f8099e 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 049bf0ce233..f38db0d887c 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 21a02909ea2..ea5bfe2742f 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;