mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

print bitblasted constraints

Browse source
This commit is contained in:
Jakob Rath 2022-12-15 13:43:09 +01:00
parent 5de0007157
commit a6504785b5
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/univariate/univariate_solver.cpp
View file

@ -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 {