Skip to content

Commit ffc696e

Browse files
exclude built-in functions from model
Signed-off-by: Nikolaj Bjorner <[email protected]>
1 parent eea0413 commit ffc696e

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/cmd_context/cmd_context.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1691,7 +1691,7 @@ void cmd_context::display_model(model_ref& mdl) {
16911691
void cmd_context::add_declared_functions(model& mdl) {
16921692
for (auto const& kv : m_func_decls) {
16931693
func_decl* f = kv.m_value.first();
1694-
if (!mdl.has_interpretation(f)) {
1694+
if (f->get_family_id() == null_family_id && !mdl.has_interpretation(f)) {
16951695
expr* val = mdl.get_some_value(f->get_range());
16961696
if (f->get_arity() == 0) {
16971697
mdl.register_decl(f, val);

0 commit comments

Comments
 (0)