From 947fe2ff9c7451d2f192d3453ed4d1eb347cd0f3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 17 Jan 2019 16:35:07 -0800
Subject: [PATCH] fix datatype occurs check bug reported by Gerhard Schellhorn

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

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 38a25c874..f9df954fa 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3919,7 +3919,6 @@ namespace smt {
                 !m_manager.proofs_enabled() &&
                 m_units_to_reassert.size() < m_fparams.m_delay_units_threshold;
 
-            TRACE("conflict", tout << delay_forced_restart << "\n";);
             if (delay_forced_restart) {
                 new_lvl = conflict_lvl - 1;
             }