From 3d995648eea72722cee40bd51694c2b2a2d3f374 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 7 Aug 2014 20:39:20 +0900
Subject: [PATCH] partial fix to model generation bug for non-linear
 constraints: avoid epsilon refinment for non-shared variables

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_arith.h      |  1 +
 src/smt/theory_arith_core.h |  3 ++-
 src/smt/theory_arith_nl.h   | 12 ++++++++----
 3 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index e7037f31a..998dd72e6 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -85,6 +85,7 @@ namespace smt {
         typedef typename Ext::numeral     numeral;
         typedef typename Ext::inf_numeral inf_numeral;
         typedef vector<numeral> numeral_vector; 
+        typedef map<rational, theory_var, obj_hash<rational>, default_eq<rational> > rational2var;
 
         static const int    dead_row_id = -1;
     protected:
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 195d78e25..fbc043048 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -2780,7 +2780,6 @@ namespace smt {
     */
     template<typename Ext>
     void theory_arith<Ext>::refine_epsilon() {
-        typedef map<rational, theory_var, obj_hash<rational>, default_eq<rational> > rational2var;
         while (true) {
             rational2var mapping;
             theory_var num = get_num_vars();
@@ -2788,6 +2787,8 @@ namespace smt {
             for (theory_var v = 0; v < num; v++) {
                 if (is_int(v))
                     continue;
+                if (!get_context().is_shared(get_enode(v)))
+                    continue;
                 inf_numeral const & val = get_value(v);
                 rational value = val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational();
                 theory_var v2;
diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index bab921ed2..d02c9e540 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -654,6 +654,7 @@ namespace smt {
         }
         return get_value(v, computed_epsilon) == val;
     }
+    
 
     /**
        \brief Return true if for every monomial x_1 * ... * x_n,
@@ -2309,8 +2310,9 @@ namespace smt {
         if (m_nl_monomials.empty())
             return FC_DONE;
 
-        if (check_monomial_assignments())
+        if (check_monomial_assignments()) {
             return FC_DONE;
+        }
 
         if (!m_params.m_nl_arith)
             return FC_GIVEUP;
@@ -2338,9 +2340,10 @@ namespace smt {
         if (!max_min_nl_vars())
             return FC_CONTINUE;
 
-        if (check_monomial_assignments())
+        if (check_monomial_assignments()) {
             return m_liberal_final_check || !m_changed_assignment ? FC_DONE : FC_CONTINUE;
-        
+        }
+
         svector<theory_var> vars;
         get_non_linear_cluster(vars);
 
@@ -2391,8 +2394,9 @@ namespace smt {
         }
         while (m_nl_strategy_idx != old_idx);
 
-        if (check_monomial_assignments())
+        if (check_monomial_assignments()) {
             return m_liberal_final_check || !m_changed_assignment ? FC_DONE : FC_CONTINUE;
+        }
 
         TRACE("non_linear", display(tout););