patch to fix #5110

Z3Prover · Apr 8, 2021 · 44156f9 · 44156f9
1 parent d91eac2
commit 44156f9
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 6 deletions.
diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
@@ -641,13 +641,13 @@ namespace datatype {
     }
 
     bool util::is_considered_uninterpreted(func_decl * f, unsigned n, expr* const* args) {
-        if (is_accessor(f)) {
-            func_decl* c = get_accessor_constructor(f);
-            SASSERT(n == 1);
-            if (is_constructor(args[0])) 
-                return to_app(args[0])->get_decl() != c;
+        if (!is_accessor(f)) 
             return false;
-        }
+        func_decl* c = get_accessor_constructor(f);
+        SASSERT(n == 1);
+        std::cout << f->get_name() << " " << mk_pp(args[0], m) << "\n";
+        if (is_constructor(args[0])) 
+            return to_app(args[0])->get_decl() != c;
         return false;
     }
 

diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
@@ -363,12 +363,17 @@ struct evaluator_cfg : public default_rewriter_cfg {
             result = m.get_some_value(f->get_range());
             return BR_DONE;
         }
+        else if (m_dt.is_accessor(f) && !is_ground(args[0])) {
+            result = m.mk_app(f, num, args);
+            return BR_DONE;            
+        }
         if (fi) {
             if (fi->is_partial())
                 fi->set_else(m.get_some_value(f->get_range()));
 
             var_subst vs(m, false);
             result = vs(fi->get_interp(), num, args);
+            std::cout << result << "\n";
             return BR_REWRITE_FULL;
         }