From 4c1fcbaa62e487c62b7cd47d2123885007b335f6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 6 Dec 2020 14:13:46 -0800 Subject: [PATCH] fix #4865 --- src/cmd_context/cmd_context.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 7c93dcfc0..8bd4b616f 100644 --- 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()))