Skip to content

Commit

Permalink
clang
Browse files Browse the repository at this point in the history
  • Loading branch information
yoni206 committed Oct 5, 2023
1 parent 94038c7 commit b4b075e
Showing 1 changed file with 8 additions and 5 deletions.
13 changes: 8 additions & 5 deletions src/theory/bv/int_blaster.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -985,18 +985,21 @@ Node IntBlaster::translateQuantifiedFormula(Node quantifiedNode)
// that involve quantified variables
std::unordered_set<Node> 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
Expand Down

0 comments on commit b4b075e

Please sign in to comment.