From a71b4fab23156b86b765896b47e762908f82949e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 27 Apr 2021 09:31:04 -0700
Subject: [PATCH] na

---
 src/sat/smt/dt_solver.cpp | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp
index 9ab23ebc8..63183ea72 100644
--- a/src/sat/smt/dt_solver.cpp
+++ b/src/sat/smt/dt_solver.cpp
@@ -717,10 +717,8 @@ namespace dt {
     }
 
     sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
-        if (!visit_rec(m, e, sign, root, redundant)) {
-            TRACE("dt", tout << mk_pp(e, m) << "\n";);
-            return sat::null_literal;
-        }
+        if (!visit_rec(m, e, sign, root, redundant)) 
+            return sat::null_literal;        
         auto lit = ctx.expr2literal(e);
         if (sign)
             lit.neg();