From 74f1358ca108f3ae4bc8b2d01a2c14e0c20bcc9b Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 4 Mar 2015 10:39:27 +0100 Subject: More work on arithmetic single invocation synthesis conjectures. --- src/theory/quantifiers/trigger.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/theory/quantifiers/trigger.cpp') diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index e953e90b2..e9ce29468 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -264,7 +264,7 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { for( std::map< Node, Node >::iterator it = m.begin(); it!=m.end(); ++it ){ if( !it->first.isNull() && it->first.getKind()==INST_CONSTANT ){ Node veq; - if( QuantArith::isolate( it->first, m, veq, n.getKind() ) ){ + if( QuantArith::isolate( it->first, m, veq, n.getKind() )!=0 ){ int vti = veq[0]==it->first ? 1 : 0; if( isUsableTrigger(veq[vti], f) && !nodeContainsVar( veq[vti], veq[vti==0 ? 1 : 0]) ){ rtr = veq; -- cgit v1.2.3