fix #3458

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

src/ast/arith_decl_plugin.h

@@ -306,14 +306,29 @@ public:
     bool is_sin(expr const* n) const { return is_app_of(n, m_afid, OP_SIN); }
     bool is_cos(expr const* n) const { return is_app_of(n, m_afid, OP_COS); }
     bool is_tan(expr const* n) const { return is_app_of(n, m_afid, OP_TAN); }
+    bool is_tanh(expr const* n) const { return is_app_of(n, m_afid, OP_TANH); }
     bool is_asin(expr const* n) const { return is_app_of(n, m_afid, OP_ASIN); }
     bool is_acos(expr const* n) const { return is_app_of(n, m_afid, OP_ACOS); }
     bool is_atan(expr const* n) const { return is_app_of(n, m_afid, OP_ATAN); }
     bool is_asinh(expr const* n) const { return is_app_of(n, m_afid, OP_ASINH); }
     bool is_acosh(expr const* n) const { return is_app_of(n, m_afid, OP_ACOSH); }
     bool is_atanh(expr const* n) const { return is_app_of(n, m_afid, OP_ATANH); }
-    bool is_pi(expr * arg) { return is_app_of(arg, m_afid, OP_PI); }
+    bool is_pi(expr const * arg) const { return is_app_of(arg, m_afid, OP_PI); }
-    bool is_e(expr * arg) { return is_app_of(arg, m_afid, OP_E); }
+    bool is_e(expr const * arg) const { return is_app_of(arg, m_afid, OP_E); }
+    bool is_non_algebraic(expr const* n) const {
+        return is_sin(n) ||
+            is_cos(n) ||
+            is_tan(n) ||
+            is_tanh(n) || 
+            is_asin(n) ||
+            is_acos(n) ||
+            is_atan(n) ||
+            is_asinh(n) ||
+            is_acosh(n) ||
+            is_atanh(n) ||
+            is_e(n) ||
+            is_pi(n);
+    }
 
     MATCH_UNARY(is_uminus);
     MATCH_UNARY(is_to_real);
@@ -350,17 +365,17 @@ class arith_util : public arith_recognizers {
 
     void init_plugin();
 
+public:
+    arith_util(ast_manager & m);
+
+    ast_manager & get_manager() const { return m_manager; }
+
     arith_decl_plugin & plugin() const {
         if (!m_plugin) const_cast<arith_util*>(this)->init_plugin();
         SASSERT(m_plugin != 0);
         return *m_plugin;
     }
 
-public:
-    arith_util(ast_manager & m);
-
-    ast_manager & get_manager() const { return m_manager; }
-
     algebraic_numbers::manager & am() {
         return plugin().am();
     }

src/cmd_context/cmd_context.cpp

@@ -1775,14 +1775,26 @@ struct contains_underspecified_op_proc {
     struct found {};
     family_id m_array_fid;
     datatype_util m_dt;
+    arith_util m_arith;
     seq_util m_seq;
     family_id m_seq_id;
     
-    contains_underspecified_op_proc(ast_manager & m):m_array_fid(m.mk_family_id("array")), m_dt(m), m_seq(m), m_seq_id(m_seq.get_family_id()) {}
+    contains_underspecified_op_proc(ast_manager & m):
+        m_array_fid(m.mk_family_id("array")), 
+        m_dt(m), 
+        m_arith(m),
+        m_seq(m), 
+        m_seq_id(m_seq.get_family_id()) {}
     void operator()(var * n)        {}
     void operator()(app * n)        {
         if (m_dt.is_accessor(n->get_decl())) 
             throw found();
+        if (n->get_family_id() == m_seq_id && m_seq.is_re(n))
+            throw found();
+        if (m_arith.plugin().is_considered_uninterpreted(n->get_decl()))
+            throw found();
+        if (m_arith.is_non_algebraic(n))
+            throw found();
         if (n->get_family_id() == m_array_fid) {
             decl_kind k = n->get_decl_kind();
             if (k == OP_AS_ARRAY ||
@@ -1791,9 +1803,6 @@ struct contains_underspecified_op_proc {
                 k == OP_CONST_ARRAY)
                 throw found();
         }
-        if (n->get_family_id() == m_seq_id && m_seq.is_re(n)) {
-            throw found();
-        }
     }
     void operator()(quantifier * n) {}
 };
@@ -1896,9 +1905,6 @@ void cmd_context::validate_model() {
                 if (m().is_true(r))
                     continue;
 
-                analyze_failure(evaluator, a, true);
-                IF_VERBOSE(11, model_smt2_pp(verbose_stream(), *this, *md, 0););                
-
                 // The evaluator for array expressions is not complete
                 // If r contains as_array/store/map/const expressions, then we do not generate the error.
                 // TODO: improve evaluator for model expressions.
@@ -1913,6 +1919,9 @@ void cmd_context::validate_model() {
                 catch (const contains_underspecified_op_proc::found &) {
                     continue;
                 }
+
+                analyze_failure(evaluator, a, true);
+                IF_VERBOSE(11, model_smt2_pp(verbose_stream(), *this, *md, 0););                
                 TRACE("model_validate", model_smt2_pp(tout, *this, *md, 0););
                 invalid_model = true;
             }

src/solver/tactic2solver.cpp

@@ -36,6 +36,8 @@ Notes:
 namespace {
 class tactic2solver : public solver_na2as {
     expr_ref_vector              m_assertions;
+    expr_ref_vector              m_last_assertions;
+    unsigned                     m_last_assertions_valid;
     unsigned_vector              m_scopes;
     ref<simple_check_sat_result> m_result;
     tactic_ref                   m_tactic;
@@ -101,7 +103,9 @@ ast_manager& tactic2solver::get_manager() const { return m_assertions.get_manage
 
 tactic2solver::tactic2solver(ast_manager & m, tactic * t, params_ref const & p, bool produce_proofs, bool produce_models, bool produce_unsat_cores, symbol const & logic):
     solver_na2as(m),
-    m_assertions(m) {
+    m_assertions(m),
+    m_last_assertions(m),
+    m_last_assertions_valid(false) {
 
     m_tactic = t;
     m_logic  = logic;
@@ -126,18 +130,21 @@ void tactic2solver::collect_param_descrs(param_descrs & r) {
 }
 
 void tactic2solver::assert_expr_core(expr * t) {
+    m_last_assertions_valid = false;
     m_assertions.push_back(t);
     m_result = nullptr;
 }
 
 
 void tactic2solver::push_core() {
+    m_last_assertions_valid = false;
     m_scopes.push_back(m_assertions.size());
     m_result = nullptr;
     TRACE("pop", tout << m_scopes.size() << "\n";);
 }
 
 void tactic2solver::pop_core(unsigned n) {
+    m_last_assertions_valid = false;
     TRACE("pop", tout << m_scopes.size() << " " << n << "\n";);
     n = std::min(m_scopes.size(), n);
     unsigned new_lvl = m_scopes.size() - n;
@@ -150,6 +157,7 @@ void tactic2solver::pop_core(unsigned n) {
 lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * assumptions) {
     if (m_tactic.get() == nullptr)
         return l_false;
+    m_last_assertions_valid = false;
     ast_manager & m = m_assertions.m();
     m_result = alloc(simple_check_sat_result, m);
     m_tactic->cleanup();
@@ -185,8 +193,9 @@ lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * as
             if (!reason_unknown.empty())
                 m_result->m_unknown = reason_unknown;
             if (num_assumptions == 0 && m_scopes.empty()) {
-                m_assertions.reset();
+                m_last_assertions.reset();
-                g->get_formulas(m_assertions);
+                g->get_formulas(m_last_assertions);
+                m_last_assertions_valid = true;
             }
             break;
         }
@@ -278,11 +287,11 @@ void tactic2solver::set_reason_unknown(char const* msg) {
 }
 
 unsigned tactic2solver::get_num_assertions() const {
-    return m_assertions.size();
+    return m_last_assertions_valid ? m_last_assertions.size() : m_assertions.size();
 }
 
 expr * tactic2solver::get_assertion(unsigned idx) const {
-    return m_assertions.get(idx);
+    return m_last_assertions_valid ? m_last_assertions.get(idx) : m_assertions.get(idx);
 }
 }