From 1a2547995acc5a98c8969e628ac5e1c45b0efe94 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 17 Jun 2016 15:55:56 -0500 Subject: Support for separation logic. Enable cbqi by default for pure BV. --- src/theory/uf/theory_uf.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/theory/uf') diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 9c461f57b..ae935798e 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -551,9 +551,9 @@ void TheoryUF::eqNotifyNewClass(TNode t) { } void TheoryUF::eqNotifyPreMerge(TNode t1, TNode t2) { - if (getLogicInfo().isQuantified()) { + //if (getLogicInfo().isQuantified()) { //getQuantifiersEngine()->getEfficientEMatcher()->merge( t1, t2 ); - } + //} } void TheoryUF::eqNotifyPostMerge(TNode t1, TNode t2) { -- cgit v1.2.3