From b4b075e042e0978322ecf2e5ed5be6e69c722530 Mon Sep 17 00:00:00 2001 From: Yoni Zohar Date: Fri, 6 Oct 2023 00:50:44 +0300 Subject: [PATCH] clang --- src/theory/bv/int_blaster.cpp | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp index 500c527fc81..ddf4f7cfd8e 100644 --- a/src/theory/bv/int_blaster.cpp +++ b/src/theory/bv/int_blaster.cpp @@ -985,18 +985,21 @@ Node IntBlaster::translateQuantifiedFormula(Node quantifiedNode) // that involve quantified variables std::unordered_set applys; expr::getKindSubterms(quantifiedNode[1], Kind::APPLY_UF, true, applys); - for (Node apply : applys) { - Trace("int-blaster-debug") << "quantified uf application: " << apply << std::endl; + for (Node apply : applys) + { + Trace("int-blaster-debug") + << "quantified uf application: " << apply << std::endl; Node f = apply.getOperator(); Trace("int-blaster-debug") << "quantified uf symbol: " << f << std::endl; TypeNode range = f.getType().getRangeType(); - if (range.isBitVector()) { + if (range.isBitVector()) + { unsigned bvsize = range.getBitVectorSize(); - rangeConstraints.push_back(mkRangeConstraint(d_intblastCache[apply], bvsize)); + rangeConstraints.push_back( + mkRangeConstraint(d_intblastCache[apply], bvsize)); } } - // the body of the quantifier Node matrix = d_intblastCache[quantifiedNode[1]]; // make the substitution