Updates to E-matching to avoid entailed instantiations earlier. Minor updates to datatypes lemmas, other minor changes.

1 files changed, 2 insertions, 2 deletions

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index b0340d630..9e0e40911 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -324,7 +324,7 @@ Node QuantifiersRewriter::computeNNF( Node body ){
     }else if( isLiteral( body[0] ) ){
       return body;
     }else{
-      std::vector< Node > children;
+      std::vector< Node > children; 
       Kind k = body[0].getKind();
 
       if( body[0].getKind()==OR || body[0].getKind()==AND ){
@@ -1546,7 +1546,7 @@ bool QuantifiersRewriter::doOperation( Node f, int computeOption, QAttributes& q
   }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
     return options::aggressiveMiniscopeQuant() && is_std;
   }else if( computeOption==COMPUTE_NNF ){
-    return options::nnfQuant();
+    return true;
   }else if( computeOption==COMPUTE_PROCESS_TERMS ){
     return true;
     //return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant();