diff options
Diffstat (limited to 'src/theory/quantifiers/quant_util.cpp')
-rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index c10f1db53..2c65b62b3 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -313,12 +313,11 @@ void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int } void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) { - Assert( n.getKind()!=IMPLIES && n.getKind()!=XOR ); newHasPol = hasPol; newPol = pol; - if( n.getKind()==NOT ){ + if( n.getKind()==NOT || ( n.getKind()==IMPLIES && child==0 ) ){ newPol = !pol; - }else if( n.getKind()==IFF ){ + }else if( n.getKind()==IFF || n.getKind()==XOR ){ newHasPol = false; }else if( n.getKind()==ITE ){ if( child==0 ){ |