From bb44b91e45fbc7eb222baae8d35af15d343cd341 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 10 Apr 2023 15:10:54 -0700
Subject: [PATCH] fix #6677

---
 src/cmd_context/cmd_context.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 1d3476b3d..c2ec7fe30 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1237,6 +1237,9 @@ bool cmd_context::try_mk_pdecl_app(symbol const & s, unsigned num_args, expr * c
     if (num_args != 1)
         return false;
 
+    if (!dt.is_datatype(args[0]->get_sort()))
+        return false;
+
     for (auto* a : dt.plugin().get_accessors(s)) {        
         fn = a->instantiate(args[0]->get_sort());
         r = m().mk_app(fn, num_args, args);