fix #4865

Z3Prover · Dec 6, 2020 · 4c1fcba · 4c1fcba
1 parent 746dd74
commit 4c1fcba
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
@@ -1759,6 +1759,8 @@ struct contains_underspecified_op_proc {
     void operator()(app * n)        {
         if (m_dt.is_accessor(n->get_decl())) 
             throw found();
+        if (m_dt.is_update_field(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()))