summaryrefslogtreecommitdiff
path: root/src/theory/arrays
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-02-26 19:11:31 -0600
committerGitHub <noreply@github.com>2020-02-26 19:11:31 -0600
commitd41d2a817f884e0f6c8d5cb3b87b4298bc1b56f5 (patch)
tree5cfe4336c5aa40cac613238a2625b1fb4aa55d31 /src/theory/arrays
parent4b7de240edeee362a0b9ca440c22a8b0744cf34b (diff)
Initial work towards -Wshadow (#3817)
Diffstat (limited to 'src/theory/arrays')
-rw-r--r--src/theory/arrays/theory_arrays.cpp5
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 534a019c3..d721b7e7a 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1327,14 +1327,15 @@ void TheoryArrays::check(Effort e) {
{
// Get all the assertions
Assertion assertion = get();
- TNode fact = assertion.assertion;
+ TNode fact = assertion.d_assertion;
Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::check(): processing " << fact << std::endl;
bool polarity = fact.getKind() != kind::NOT;
TNode atom = polarity ? fact : fact[0];
- if (!assertion.isPreregistered) {
+ if (!assertion.d_isPreregistered)
+ {
if (atom.getKind() == kind::EQUAL) {
if (!d_equalityEngine.hasTerm(atom[0])) {
Assert(atom[0].isConst());
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback