fix #6807

src/ackermannization/ackr_helper.h

@@ -18,6 +18,7 @@
 
 #include "ast/bv_decl_plugin.h"
 #include "ast/array_decl_plugin.h"
+#include "ast/ast_ll_pp.h"
 
 class ackr_helper {
 public:
@@ -40,11 +41,9 @@ public:
     inline bool is_uninterp_fn(app const * a) const {
         if (is_uninterp(a))
             return true;
-        else {
         decl_plugin * p = m_bvutil.get_manager().get_plugin(a->get_family_id());
         return p->is_considered_uninterpreted(a->get_decl());        
     }
-    }
 
     /**
        \brief determines if a term is a candidate select for Ackerman reduction
@@ -64,11 +63,10 @@ public:
             }
         }
         else {
-            for (expr* arg : *a) {
+            for (expr* arg : *a) 
                 non_select.mark(arg, true);
         }
     }
-    }
 
     void prune_non_select(obj_map<app, app_set*> & sels, expr_mark& non_select) {
         ptr_vector<app> nons;
@@ -112,7 +110,8 @@ public:
     }
 
     void insert(fun2terms_map& f2t, sel2terms_map& s2t, app* a) {
-        if (a->get_num_args() == 0) return;
+        if (a->get_num_args() == 0)
+            return;
         ast_manager& m = m_bvutil.get_manager();
         app_set* ts = nullptr;
         bool is_const_args = true;
@@ -129,22 +128,19 @@ public:
                 ts = alloc(app_set);
                 f2t.insert(fd, ts);
             }
-            is_const_args = m.is_value(a->get_arg(0));
+            is_const_args = m.is_unique_value(a->get_arg(0));
         }
-        else {
+        else 
             return;
-        }
-        for (unsigned i = 1; is_const_args && i < a->get_num_args(); ++i) {
-            is_const_args &= m.is_value(a->get_arg(i));
-        }
         
-        if (is_const_args) {
+        for (unsigned i = 1; is_const_args && i < a->get_num_args(); ++i) 
+            is_const_args &= m.is_unique_value(a->get_arg(i));
+        
+        if (is_const_args) 
             ts->const_args.insert(a);
-        }
+        else 
-        else {
             ts->var_args.insert(a);
     }
-    }
     
 private:
     bv_util                              m_bvutil;

src/ackermannization/lackr.cpp

@@ -22,6 +22,8 @@
 #include "ackermannization/ackr_info.h"
 #include "ast/for_each_expr.h"
 #include "ast/ast_util.h"
+#include "ast/ast_pp.h"
+#include "ast/ast_ll_pp.h"
 #include "model/model_smt2_pp.h"
 
 lackr::lackr(ast_manager& m, const params_ref& p, lackr_stats& st,
@@ -142,10 +144,10 @@ bool lackr::ackr(app * const t1, app * const t2) {
 // Introduce the ackermann lemma for each pair of terms.
 //
 void lackr::eager_enc() {
-    TRACE("ackermannize", tout << "#funs: " << m_fun2terms.size() << "#sels: " << m_sel2terms.size() << std::endl;);
+    TRACE("ackermannize", tout << "#funs: " << m_fun2terms.size() << " #sels: " << m_sel2terms.size() << std::endl;);
-    for (auto const& kv : m_fun2terms) {
+    for (auto const& [k,v] : m_fun2terms) {
         checkpoint();
-        ackr(kv.get_value());
+        ackr(v);
     }
     for (auto const& kv : m_sel2terms) {
         checkpoint();
@@ -172,14 +174,13 @@ void lackr::ackr(app_set const* ts) {
 }
 
 void lackr::abstract_fun(fun2terms_map const& apps) {
-    for (auto const& kv : apps) {
+    for (auto const& [fd, v] : apps) {
-        func_decl* fd = kv.m_key;
+        for (app * t : v->var_args) {
-        for (app * t : kv.m_value->var_args) {
             app * fc = m.mk_fresh_const(fd->get_name(), t->get_sort());
             SASSERT(t->get_decl() == fd);
             m_info->set_abstr(t, fc);
         }
-        for (app * t : kv.m_value->const_args) {
+        for (app * t : v->const_args) {
             app * fc = m.mk_fresh_const(fd->get_name(), t->get_sort());
             SASSERT(t->get_decl() == fd);
             m_info->set_abstr(t, fc);

src/ast/array_decl_plugin.cpp

@@ -633,6 +633,12 @@ bool array_decl_plugin::is_value(app * _e) const {
     }
 }
 
+bool array_decl_plugin::is_unique_value(app* _e) const {
+    array_util u(*m_manager);
+    expr* e = _e;
+    return u.is_const(e, e) && m_manager->is_unique_value(e);
+}
+
 
 func_decl * array_recognizers::get_as_array_func_decl(expr * n) const { 
     SASSERT(is_as_array(n)); 

src/ast/array_decl_plugin.h

@@ -137,6 +137,8 @@ class array_decl_plugin : public decl_plugin {
 
     bool is_value(app * e) const override;
 
+    bool is_unique_value(app* e) const override;
+
 };
 
 class array_recognizers {