From 6c24a70c44aeab3d3de78f8af71fce454cd02342 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 2 May 2023 13:05:08 -0700
Subject: [PATCH] remove debug output

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/cmd_context.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index a4adbb0ed76..8d1e375d101 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -2006,7 +2006,6 @@ void cmd_context::complete_model(model_ref& md) const {
                 md->register_decl(f, body);
         }
     }
-    verbose_stream() << *md << "\n";
 }
 
 /**