From 3487b368d1413cdff2de9f269a76f7ab92148ec9 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 17 Aug 2017 17:27:06 +0100 Subject: [PATCH] Added diagnostic output for pattern inference. --- src/ast/pattern/pattern_inference.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp index 11268b2f3..d97c2f094 100644 --- a/src/ast/pattern/pattern_inference.cpp +++ b/src/ast/pattern/pattern_inference.cpp @@ -729,6 +729,12 @@ void pattern_inference::reduce1_quantifier(quantifier * q) { return; } + IF_IVERBOSE(10, + verbose_stream() << "(smt.inferred-patterns :qid " << q->get_qid() << "\n"; + for (unsigned i = 0; i < new_patterns.size(); i++) + verbose_stream() << " " << mk_ismt2_pp(new_patterns[i], m, 2) << "\n"; + verbose_stream() << ")\n"; ); + cache_result(q, new_q, pr); }