From d6643e4db92c041b4496539696e6a5bdf330a727 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 12 Nov 2022 17:53:53 +0000 Subject: [PATCH] CHC solver: add constraint to verbose output The verbose output now includes the constraint that is used when propagating a candidate invariant. --- src/cprover/propagate.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/cprover/propagate.cpp b/src/cprover/propagate.cpp index 9c3edac5688..7fe5410e883 100644 --- a/src/cprover/propagate.cpp +++ b/src/cprover/propagate.cpp @@ -43,6 +43,15 @@ void propagate( for(const auto &implication : f.implications) { + if(verbose) + { + std::cout << consolet::green; + std::cout << 'C' << consolet::faint << std::setw(2) << work.frame.index + << consolet::reset << ' '; + std::cout << consolet::green << format(implication.as_expr()); + std::cout << consolet::reset << '\n'; + } + auto &next_state = implication.rhs.arguments().front(); auto lambda_expr = lambda_exprt({state_expr()}, work.invariant); auto instance = lambda_expr.instantiate({next_state});