diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2014-09-17 15:01:19 -0700 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2014-10-02 13:28:22 -0700 |
| commit | 4c32421fee453d82e6c1d7d3dc1605da11db1a09 (patch) | |
| tree | b0e4689aac85a856db5e75513610d53475fc4f7d /src/theory/theory_engine.cpp | |
| parent | 3df8013300486129fc06f3a20d43def1f34a221a (diff) | |
More model-based combination for arrays
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index ffe4258cd..b943a7ee5 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -501,8 +501,8 @@ void TheoryEngine::combineTheories() { // We need to split on it Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl; lemma(equality.orNode(equality.notNode()), false, false, false, carePair.theory); - if (false) { - if (es == EQUALITY_TRUE_IN_MODEL) { + if (true) { + if (es == EQUALITY_TRUE || es == EQUALITY_TRUE_IN_MODEL) { Node e = ensureLiteral(equality); d_propEngine->requirePhase(e, true); } |