From 7fd1c171cec343a3640e754c33cd45ff2a9f9f2c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 1 Jan 2024 19:11:24 -0800
Subject: [PATCH] na

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

diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp
index 696816c79..09c116b3c 100644
--- a/src/sat/smt/polysat_solver.cpp
+++ b/src/sat/smt/polysat_solver.cpp
@@ -341,6 +341,7 @@ namespace polysat {
                 TRACE("bv", tout << "literal is true " << ctx.literal2expr(lit) << "\n");
                 return false;
             }
+        TRACE("bv", tout << name << ": "; for (auto lit : lits) tout << ctx.literal2expr(lit) << " "; tout << "\n");
         validate_axiom(lits);
         s().add_clause(lits.size(), lits.data(), sat::status::th(is_redundant, get_id(), hint));
         return true;