1 files changed, 35 insertions, 26 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 014d3c603..3c3bbe971 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -77,6 +77,7 @@
 #include "prop/options.h"
 #include "theory/arrays/options.h"
 #include "util/sort_inference.h"
+#include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/quantifiers/macros.h"
 #include "theory/datatypes/options.h"
 #include "theory/quantifiers/first_order_reasoning.h"
@@ -1149,6 +1150,10 @@ void SmtEngine::setLogicInternal() throw() {
       options::mbqiMode.set( quantifiers::MBQI_FMC );
     }
   }
+  if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){
+    //must do pre-skolemization
+    options::preSkolemQuant.set( true );
+  }
   if( options::ufssSymBreak() ){
     options::sortInference.set( true );
   }
@@ -3042,35 +3047,35 @@ void SmtEnginePrivate::processAssertions() {
       d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] );
     }
   }
-
-  dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess);
-  if( options::preSkolemQuant() ){
-    //apply pre-skolemization to existential quantifiers
-    for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
-      Node prev = d_assertionsToPreprocess[i];
-      vector< Node > fvs;
-      d_assertionsToPreprocess[i] = Rewriter::rewrite( preSkolemizeQuantifiers( d_assertionsToPreprocess[i], true, fvs ) );
-      if( prev!=d_assertionsToPreprocess[i] ){
-        Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << endl;
-        Trace("quantifiers-rewrite") << "   ...got " << d_assertionsToPreprocess[i] << endl;
+  if( d_smt.d_logic.isQuantified() ){
+    dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess);
+    if( options::preSkolemQuant() ){
+      //apply pre-skolemization to existential quantifiers
+      for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
+        Node prev = d_assertionsToPreprocess[i];
+        vector< Node > fvs;
+        d_assertionsToPreprocess[i] = Rewriter::rewrite( preSkolemizeQuantifiers( d_assertionsToPreprocess[i], true, fvs ) );
+        if( prev!=d_assertionsToPreprocess[i] ){
+          Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << endl;
+          Trace("quantifiers-rewrite") << "   ...got " << d_assertionsToPreprocess[i] << endl;
+        }
       }
     }
-  }
-  dumpAssertions("post-skolem-quant", d_assertionsToPreprocess);
-
-  if( options::macrosQuant() ){
-    //quantifiers macro expansion
-    bool success;
-    do{
-      QuantifierMacros qm;
-      success = qm.simplify( d_assertionsToPreprocess, true );
-    }while( success );
-  }
+    dumpAssertions("post-skolem-quant", d_assertionsToPreprocess);
+    if( options::macrosQuant() ){
+      //quantifiers macro expansion
+      bool success;
+      do{
+        QuantifierMacros qm;
+        success = qm.simplify( d_assertionsToPreprocess, true );
+      }while( success );
+    }
 
-  Trace("fo-rsn-enable") << std::endl;
-  if( options::foPropQuant() ){
-    FirstOrderPropagation fop;
-    fop.simplify( d_assertionsToPreprocess );
+    Trace("fo-rsn-enable") << std::endl;
+    if( options::foPropQuant() ){
+      FirstOrderPropagation fop;
+      fop.simplify( d_assertionsToPreprocess );
+    }
   }
 
   if( options::sortInference() ){
@@ -3078,6 +3083,10 @@ void SmtEnginePrivate::processAssertions() {
     d_smt.d_theoryEngine->getSortInference()->simplify( d_assertionsToPreprocess );
   }
 
+  //if( options::quantConflictFind() ){
+  //  d_smt.d_theoryEngine->getQuantConflictFind()->registerAssertions( d_assertionsToPreprocess );
+  //}
+
   dumpAssertions("pre-simplify", d_assertionsToPreprocess);
   Chat() << "simplifying assertions..." << endl;
   bool noConflict = simplifyAssertions();