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