diff options
Diffstat (limited to 'src/theory/quantifiers/fmf/bounded_integers.cpp')
| -rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 3ade304e8..e8b9f5dea 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -783,7 +783,8 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node Node tu = u; getBounds( q, v, rsi, tl, tu ); Assert(!tl.isNull() && !tu.isNull()); - if( ra==d_quantEngine->getTermUtil()->d_true ){ + if (ra.isConst() && ra.getConst<bool>()) + { long rr = range.getConst<Rational>().getNumerator().getLong()+1; Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl; for( unsigned k=0; k<rr; k++ ){ |