From 3b8c0b7ae61fb06cf7e5d521268e5b4c2dfd06e8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 24 Jan 2022 15:11:24 +0100
Subject: [PATCH] fix #5791

---
 src/ast/datatype_decl_plugin.cpp | 13 +++++++------
 src/ast/datatype_decl_plugin.h   |  7 ++++---
 2 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index ce183ce6b..ace0cb567 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -580,7 +580,7 @@ namespace datatype {
             m_defs.remove(s);
         }
 
-        bool plugin::is_value_visit(expr * arg, ptr_buffer<app> & todo) const {
+        bool plugin::is_value_visit(bool unique, expr * arg, ptr_buffer<app> & todo) const {
             if (!is_app(arg))
                 return false;
             family_id fid = to_app(arg)->get_family_id();
@@ -592,12 +592,13 @@ namespace datatype {
                 todo.push_back(to_app(arg));
                 return true;
             }
-            else {
+            else if (unique)
+                return m_manager->is_unique_value(arg);
+            else 
                 return m_manager->is_value(arg);
-            }
         }
         
-        bool plugin::is_value(app * e) const {
+        bool plugin::is_value_aux(bool unique, app * e) const {
             TRACE("dt_is_value", tout << "checking\n" << mk_ismt2_pp(e, *m_manager) << "\n";);
             if (!u().is_constructor(e))
                 return false;
@@ -608,7 +609,7 @@ namespace datatype {
             ptr_buffer<app> todo;
             // potentially expensive check for common sub-expressions.
             for (expr* arg : *e) {
-                if (!is_value_visit(arg, todo)) {
+                if (!is_value_visit(unique, arg, todo)) {
                     TRACE("dt_is_value", tout << "not-value:\n" << mk_ismt2_pp(arg, *m_manager) << "\n";);
                     return false;
                 }
@@ -618,7 +619,7 @@ namespace datatype {
                 SASSERT(u().is_constructor(curr));
                 todo.pop_back();
                 for (expr* arg : *curr) {
-                    if (!is_value_visit(arg, todo)) {
+                    if (!is_value_visit(unique, arg, todo)) {
                         TRACE("dt_is_value", tout << "not-value:\n" << mk_ismt2_pp(arg, *m_manager) << "\n";);
                         return false;
                     }
diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
index d4d38a757..0172d0b1d 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -230,9 +230,9 @@ namespace datatype {
         
             bool is_fully_interp(sort * s) const override;
         
-            bool is_value(app* e) const override;
+            bool is_value(app* e) const override { return is_value_aux(false, e); }
         
-            bool is_unique_value(app * e) const override { return is_value(e); }
+            bool is_unique_value(app * e) const override { return is_value_aux(true, e); }
         
             void get_op_names(svector<builtin_name> & op_names, symbol const & logic) override;
                 
@@ -257,7 +257,8 @@ namespace datatype {
             bool has_nested_arrays() const { return m_has_nested_arrays; }
 
         private:
-            bool is_value_visit(expr * arg, ptr_buffer<app> & todo) const;
+            bool is_value_visit(bool unique, expr * arg, ptr_buffer<app> & todo) const;
+            bool is_value_aux(bool unique, app * arg) const;
         
             func_decl * mk_update_field(
                 unsigned num_parameters, parameter const * parameters,