ite removal option for quantifiers --ite-remove-quant, e-matching for boolean terms, improvement for pre skolemization

1 files changed, 8 insertions, 4 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index a11cc85c0..f12143bbe 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -583,12 +583,16 @@ bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
     return true;
   }else{
     eq::EqualityEngine* ee = getEngine();
-    if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
-      if( ee->areEqual( a, b ) ){
-        return true;
+    if( d_liberal ){
+      return true;//!areDisequal( a, b );
+    }else{
+      if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
+        if( ee->areEqual( a, b ) ){
+          return true;
+        }
       }
+      return false;
     }
-    return false;
   }
 }