From 3f19c12a12de86c48fbd139af228490df3d1b5c9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 8 Dec 2017 05:48:34 +0530
Subject: [PATCH 1/2] add obj_ref_map to make it easier to maintain reference
 counts with a map of objects

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/util/obj_ref_hashtable.h | 111 +++++++++++++++++++++++++++++++++++
 1 file changed, 111 insertions(+)
 create mode 100644 src/util/obj_ref_hashtable.h

diff --git a/src/util/obj_ref_hashtable.h b/src/util/obj_ref_hashtable.h
new file mode 100644
index 000000000..6bd4f1556
--- /dev/null
+++ b/src/util/obj_ref_hashtable.h
@@ -0,0 +1,111 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    obj_ref_hashtable.h
+
+Abstract:
+
+    corresponding obj_map with reference count managment.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2017-12-8
+
+Revision History:
+
+--*/
+#ifndef OBJ_REF_HASHTABLE_H_
+#define OBJ_REF_HASHTABLE_H_
+
+#include "util/obj_hashtable.h"
+
+template<typename M, typename Key, typename Value>
+class obj_ref_map {
+    M&                  m;
+    obj_map<Key, Value> m_table;
+public:
+    obj_ref_map(M& m):m(m) {}
+    
+    ~obj_ref_map() { reset();  }
+
+    void reset() {
+        for (auto& kv : m_table) {
+            m.dec_ref(kv.m_key);
+        }
+        m_table.reset();
+    }
+
+    void finalize() {
+        reset();
+        m_table.finalize();
+    }
+
+    bool empty() const { return m_table.empty(); }
+
+    unsigned size() const { return m_table.size();  }
+    
+    unsigned capacity() const { return m_table.capacity();  }
+    
+    iterator begin() const { return m_table.begin(); }
+    
+    iterator end() const { return m_table.end();  }
+    
+    void insert(Key * const k, Value const & v) {
+        if (!m_table.contains(k)) m.inc_ref(k);
+        m_table.insert(k, v);
+    }
+
+    void insert(Key * const k, Value && v) {
+        if (!m_table.contains(k)) m.inc_ref(k);
+        m_table.insert(k, v);
+    }
+    
+    key_data const & insert_if_not_there(Key * k, Value const & v) {
+        if (!m_table.contains(k)) m.inc_ref(k);
+        return m_table.insert_if_not_there(k, v);
+    }
+
+    obj_map_entry * insert_if_not_there2(Key * k, Value const & v) {
+        if (!m_table.contains(k)) m.inc_ref(k);
+        return m_table.insert_if_not_there2(k, v);
+    }
+    
+    obj_map_entry * find_core(Key * k) const { return m_table.find_core(k); }
+
+    bool find(Key * const k, Value & v) const { return m_table.find(k, v); }
+
+    value const & find(key * k) const { return m_table.find(k); }
+
+    value & find(key * k)  { return m_table.find(k); }
+
+    value const & operator[](key * k) const { return find(k); }
+
+    value & operator[](key * k) { return find(k); }
+    
+    iterator find_iterator(Key * k) const { return m_table.find_iterator(k); }
+
+    bool contains(Key * k) const { return m_table.contains(k); }
+
+    void remove(Key * k) { 
+        if (m_table.contains(k)) {
+            m_table.remove(k);
+            m.dec_ref(k);
+        }
+    }
+    
+    void erase(Key * k) { remove(k); }
+
+    unsigned long long get_num_collision() const { return m_table.get_num_collision(); }
+
+    void swap(obj_ref_map & other) {
+        m_table.swap(other.m_table);
+    }
+
+    
+};
+
+
+#endif /* OBJ_REF_HASHTABLE_H_ */
+

From a5d5dfdf86c507e300a11b37f161bb9587e988e5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 8 Dec 2017 09:23:57 +0530
Subject: [PATCH 2/2] fix setup for non-linear real arithmetic per QF_UFNRA
 regresssions

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/static_features.cpp | 14 +++-----------
 src/smt/smt_setup.cpp       |  2 +-
 2 files changed, 4 insertions(+), 12 deletions(-)

diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp
index 3db4d02a2..9f52ea9a5 100644
--- a/src/ast/static_features.cpp
+++ b/src/ast/static_features.cpp
@@ -111,16 +111,6 @@ void static_features::flush_cache() {
     m_expr2formula_depth.reset();
 }
 
-#if 0
-bool static_features::is_non_linear(expr * e) const {
-    if (!is_arith_expr(e))
-        return false;
-    if (is_numeral(e))
-        return true;
-    if (m_autil.is_add(e))
-        return true; // the non
-} 
-#endif
 
 bool static_features::is_diff_term(expr const * e, rational & r) const {
     // lhs can be 'x' or '(+ k x)'
@@ -301,10 +291,12 @@ void static_features::update_core(expr * e) {
                 m_num_interpreted_constants++;
         }
         if (fid == m_afid) {
+            // std::cout << mk_pp(e, m_manager) << "\n";
             switch (to_app(e)->get_decl_kind()) {
             case OP_MUL:
-                if (!is_numeral(to_app(e)->get_arg(0)))
+                if (!is_numeral(to_app(e)->get_arg(0)) || to_app(e)->get_num_args() > 2) {
                     m_num_non_linear++;
+                }
                 break;
             case OP_DIV:
             case OP_IDIV:
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 631805b4d..bbc91e4c6 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -968,7 +968,7 @@ namespace smt {
         if (st.num_theories() == 2 && st.has_uf() && is_arith(st)) {
             if (!st.m_has_real)
                 setup_QF_UFLIA(st);
-            else if (!st.m_has_int)
+            else if (!st.m_has_int && st.m_num_non_linear == 0)
                 setup_QF_UFLRA();
             else
                 setup_unknown();