mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
update diagnostics
This commit is contained in:
parent
138f0d269c
commit
a0d4a8c21c
|
@ -23,6 +23,7 @@ Revision History:
|
|||
#include "ast/rewriter/var_subst.h"
|
||||
#include "smt/smt_context.h"
|
||||
#include "smt/qi_queue.h"
|
||||
#include <iostream>
|
||||
|
||||
namespace smt {
|
||||
|
||||
|
@ -228,15 +229,12 @@ namespace smt {
|
|||
|
||||
|
||||
TRACE("qi_queue", tout << "new instance:\n" << mk_pp(instance, m) << "\n";);
|
||||
TRACE("qi_queue_instance", tout << "new instance:\n" << mk_pp(instance, m) << "\n";);
|
||||
expr_ref s_instance(m);
|
||||
proof_ref pr(m);
|
||||
m_context.get_rewriter()(instance, s_instance, pr);
|
||||
|
||||
TRACE("qi_queue_bug", tout << "new instance after simplification:\n" << s_instance << "\n";);
|
||||
if (m.is_true(s_instance)) {
|
||||
TRACE("checker", tout << "reduced to true, before:\n" << mk_ll_pp(instance, m););
|
||||
|
||||
STRACE("instance", tout << "Instance reduced to true\n";);
|
||||
stat -> inc_num_instances_simplify_true();
|
||||
if (m.has_trace_stream()) {
|
||||
|
@ -250,9 +248,11 @@ namespace smt {
|
|||
std::cout << "instantiate\n";
|
||||
enode_vector _bindings(num_bindings, bindings);
|
||||
for (auto * b : _bindings)
|
||||
std::cout << enode_pp(b, m_context) << " ";
|
||||
std::cout << mk_pp(b->get_expr(), m) << " ";
|
||||
std::cout << "\n";
|
||||
std::cout << mk_pp(q, m) << "\n";
|
||||
std::cout << "instance\n";
|
||||
std::cout << instance << "\n";
|
||||
#endif
|
||||
|
||||
TRACE("qi_queue", tout << "simplified instance:\n" << s_instance << "\n";);
|
||||
|
|
Loading…
Reference in a new issue