From a6504785b5f8e7e967fa4144dee0f0a30339ab3b Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 15 Dec 2022 13:43:09 +0100 Subject: [PATCH] print bitblasted constraints --- src/math/polysat/univariate/univariate_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/polysat/univariate/univariate_solver.cpp b/src/math/polysat/univariate/univariate_solver.cpp index f9091fa1e..e00777ab8 100644 --- a/src/math/polysat/univariate/univariate_solver.cpp +++ b/src/math/polysat/univariate/univariate_solver.cpp @@ -85,7 +85,7 @@ namespace polysat { e = m.mk_not(e); expr* a = m.mk_const(m.mk_const_decl(symbol(dep), m.mk_bool_sort())); s->assert_expr(e, a); - // std::cout << "add: " << expr_ref(e, m) << " <== " << expr_ref(a, m) << "\n"; + IF_VERBOSE(10, verbose_stream() << "(assert (! " << expr_ref(e, m) << " :named " << expr_ref(a, m) << "))\n"); } void add_ule(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) override {