Change default option of simple ite lifting within quantifier bodies. add some debug messages.

4 files changed, 7 insertions, 1 deletions

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 13e075265..e1e2f96c2 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -290,6 +290,8 @@ void BoundedIntegers::registerQuantifier( Node f ) {
           }
         }
       }
+    }else{
+      Trace("bound-int-warn") << "Warning : Bounded Integers : Could not find bounds for " << f << std::endl;
     }
   }
 }
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index a0b195a9c..cdf697675 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -854,6 +854,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
       }
     }
     if( !success ){
+      Trace("fmc-warn") << "WARNING : ARRAYS : Can't process base array " << r << std::endl;
       Trace("fmc-debug") << "Can't process base array " << r << std::endl;
       //can't process this array
       d.reset();
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 1c5e52869..57211ade7 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -27,6 +27,9 @@ option prenexQuant /--disable-prenex-quant bool :default true
 option varElimQuant /--disable-var-elim-quant bool :default true
  disable simple variable elimination for quantified formulas
 
+option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true
+ disable simple ite lifting for quantified formulas
+
 # Whether to CNF quantifier bodies
 option cnfQuant --cnf-quant bool :default false
  apply CNF conversion to quantified formulas
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index b08752169..e27897a96 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -914,7 +914,7 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption
   }else if( computeOption==COMPUTE_NNF ){
     return false;//TODO: compute NNF (current bad idea since arithmetic rewrites equalities)
   }else if( computeOption==COMPUTE_SIMPLE_ITE_LIFT ){
-    return !options::finiteModelFind();
+    return options::simpleIteLiftQuant();//!options::finiteModelFind();
   }else if( computeOption==COMPUTE_PRENEX ){
     return options::prenexQuant() && !options::aggressiveMiniscopeQuant();
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){