diff options
Diffstat (limited to 'src/theory/uf/theory_uf.cpp')
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index a58834891..0a48d4c71 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -90,8 +90,7 @@ void TheoryUF::finishInit() { if (options::finiteModelFind() && options::ufssMode() != options::UfssMode::NONE) { - d_thss.reset(new CardinalityExtension( - getSatContext(), getUserContext(), *d_out, this)); + d_thss.reset(new CardinalityExtension(d_state, d_im, this)); } // The kinds we are treating as function application in congruence d_equalityEngine->addFunctionKind(kind::APPLY_UF, false, options::ufHo()); @@ -136,10 +135,6 @@ void TheoryUF::postCheck(Effort level) if (d_thss != nullptr) { d_thss->check(level); - if (d_thss->isConflict()) - { - d_state.notifyInConflict(); - } } // check with the higher-order extension if (!d_state.isInConflict() && fullEffort(level)) @@ -159,9 +154,8 @@ bool TheoryUF::preNotifyFact( bool isDecision = d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact); d_thss->assertNode(fact, isDecision); - if (d_thss->isConflict()) + if (d_state.isInConflict()) { - d_state.notifyInConflict(); return true; } } |