summaryrefslogtreecommitdiff
path: root/src/smt_util
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/smt_util
parent550c49a7dd2b13ea29743458336f0c0a0fb6099a (diff)
Rename CVC4_ macros to CVC5_. (#6327)
Diffstat (limited to 'src/smt_util')
-rw-r--r--src/smt_util/boolean_simplification.h6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/smt_util/boolean_simplification.h b/src/smt_util/boolean_simplification.h
index ef0c3f3de..fb3b90deb 100644
--- a/src/smt_util/boolean_simplification.h
+++ b/src/smt_util/boolean_simplification.h
@@ -39,7 +39,7 @@ class BooleanSimplification {
static bool push_back_associative_commute_recursive(
Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode)
- CVC4_WARN_UNUSED_RESULT;
+ CVC5_WARN_UNUSED_RESULT;
public:
/**
@@ -165,8 +165,8 @@ class BooleanSimplification {
AssertArgument(n.getKind() == k, n,
"expected node to have kind %s", kindToString(k).c_str());
- bool b CVC4_UNUSED =
- push_back_associative_commute_recursive(n, buffer, k, notK, false);
+ bool b CVC5_UNUSED =
+ push_back_associative_commute_recursive(n, buffer, k, notK, false);
if(buffer.size() == 0) {
// all the TRUEs for an AND (resp FALSEs for an OR) were simplified away
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback