diff options
Diffstat (limited to 'src/theory/theory.cpp')
| -rw-r--r-- | src/theory/theory.cpp | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index d69c6edc5..3c603051c 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -23,6 +23,7 @@ #include "base/check.h" #include "expr/node_algorithm.h" +#include "options/smt_options.h" #include "options/theory_options.h" #include "smt/smt_statistics_registry.h" #include "theory/ext_theory.h" @@ -81,8 +82,7 @@ Theory::Theory(TheoryId id, d_equalityEngine(nullptr), d_allocEqualityEngine(nullptr), d_theoryState(nullptr), - d_inferManager(nullptr), - d_proofsEnabled(false) + d_inferManager(nullptr) { smtStatisticsRegistry()->registerStat(&d_checkTime); smtStatisticsRegistry()->registerStat(&d_computeCareGraphTime); @@ -296,12 +296,12 @@ void Theory::computeCareGraph() { switch (d_valuation.getEqualityStatus(a, b)) { case EQUALITY_TRUE_AND_PROPAGATED: case EQUALITY_FALSE_AND_PROPAGATED: - // If we know about it, we should have propagated it, so we can skip - break; + // If we know about it, we should have propagated it, so we can skip + break; default: - // Let's split on it - addCarePair(a, b); - break; + // Let's split on it + addCarePair(a, b); + break; } } } |