diff options
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 4 |
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(); |