diff options
| -rw-r--r-- | src/theory/datatypes/datatypes_sygus.cpp | 4 | ||||
| -rw-r--r-- | src/theory/quantifiers/extended_rewrite.cpp | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index a6a3ffc9d..1d1d2c2be 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -1223,8 +1223,8 @@ void SygusSymBreakNew::incrementCurrentSearchSize( Node m, std::vector< Node >& for (const TNode& t : itt->second) { if (!options::sygusSymBreakLazy() - || d_active_terms.find(t) != d_active_terms.end() - && !it->second.empty()) + || (d_active_terms.find(t) != d_active_terms.end() + && !it->second.empty())) { Node rlv = getRelevancyCondition(t); std::unordered_map<TNode, TNode, TNodeHashFunction> cache; diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index e64e1b7b2..ab292e7bb 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -787,8 +787,8 @@ Node ExtendedRewriter::extendedRewriteBcp( // also, treat it as clause if possible if (cln.getNumChildren() > 0 - & (bcp_kinds.empty() - || bcp_kinds.find(cln.getKind()) != bcp_kinds.end())) + && (bcp_kinds.empty() + || bcp_kinds.find(cln.getKind()) != bcp_kinds.end())) { if (std::find(clauses.begin(), clauses.end(), cn) == clauses.end() && prop_clauses.find(cn) == prop_clauses.end()) |