diff options
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.cpp')
| -rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 7365960e9..1475446fe 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -67,12 +67,10 @@ TheoryQuantifiers::~TheoryQuantifiers() { void TheoryQuantifiers::finishInit() { // quantifiers are not evaluated in getModelValue - TheoryModel* tm = d_valuation.getModel(); - Assert(tm != nullptr); - tm->setUnevaluatedKind(EXISTS); - tm->setUnevaluatedKind(FORALL); + d_valuation.setUnevaluatedKind(EXISTS); + d_valuation.setUnevaluatedKind(FORALL); // witness is used in several instantiation strategies - tm->setUnevaluatedKind(WITNESS); + d_valuation.setUnevaluatedKind(WITNESS); } void TheoryQuantifiers::preRegisterTerm(TNode n) { |