diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-03-04 10:39:27 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-03-04 10:39:38 +0100 |
| commit | 74f1358ca108f3ae4bc8b2d01a2c14e0c20bcc9b (patch) | |
| tree | ffcd22bc1205e4619e05af2eac79918287af2374 /src/theory/quantifiers/trigger.cpp | |
| parent | f6833bca76627f970d3c61ee163a32869ffa1b10 (diff) | |
More work on arithmetic single invocation synthesis conjectures.
Diffstat (limited to 'src/theory/quantifiers/trigger.cpp')
| -rw-r--r-- | src/theory/quantifiers/trigger.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
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; |