summaryrefslogtreecommitdiff
path: root/src/theory/uf/symmetry_breaker.cpp
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2021-04-09 17:22:07 -0700
committerGitHub <noreply@github.com>2021-04-09 17:22:07 -0700
commitf87f038c5f0821d0fefb01cea00bfdec6004da91 (patch)
treed948178e1c0d2dc459a976f0d187d2d41a5437c0 /src/theory/uf/symmetry_breaker.cpp
parent550c49a7dd2b13ea29743458336f0c0a0fb6099a (diff)
Rename CVC4_ macros to CVC5_. (#6327)
Diffstat (limited to 'src/theory/uf/symmetry_breaker.cpp')
-rw-r--r--src/theory/uf/symmetry_breaker.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index 0586da6a0..b52e39ebc 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -370,7 +370,7 @@ Node SymmetryBreaker::normInternal(TNode n, size_t level) {
Debug("ufsymm:eq") << "UFSYMM " << n[0] << " <==> " << n[1] << endl;
}
}
- CVC4_FALLTHROUGH;
+ CVC5_FALLTHROUGH;
case kind::XOR:
// commutative binary operator handling
return n[1] < n[0] ? NodeManager::currentNM()->mkNode(k, n[1], n[0]) : Node(n);
@@ -438,7 +438,7 @@ void SymmetryBreaker::assertFormula(TNode phi) {
d_permutations.insert(p);
}
d_template.reset();
- bool good CVC4_UNUSED = d_template.match(phi);
+ bool good CVC5_UNUSED = d_template.match(phi);
Assert(good);
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback