diff options
Diffstat (limited to 'src/theory/quantifiers/equality_query.cpp')
| -rw-r--r-- | src/theory/quantifiers/equality_query.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index 1d582f597..ac07e13fb 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -67,7 +67,9 @@ bool EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) { } Trace("term-db-lemma") << " add split on : " << eq << std::endl; } - d_qe->addSplit( eq ); + eq = Rewriter::rewrite(eq); + Node split = NodeManager::currentNM()->mkNode(OR, eq, eq.negate()); + d_qe->addLemma(split); return false; }else{ ee->assertEquality( eq, true, eq_exp ); |