prepare release

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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"

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);

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;