diff options
Diffstat (limited to 'src/theory/rep_set.cpp')
-rw-r--r-- | src/theory/rep_set.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 647ef965a..800e007f7 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -278,7 +278,12 @@ bool RepSetIterator::resetIndex( int i, bool initial ) { Node range = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS, u, l ) ); Node ra = Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ, range, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) ); d_domain[ii].clear(); - d_lower_bounds[ii] = l; + Node tl = l; + Node tu = u; + if( d_qe->getBoundedIntegers() && d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][ii] ) ){ + d_qe->getBoundedIntegers()->getBounds( d_owner, d_owner[0][ii], this, tl, tu ); + } + d_lower_bounds[ii] = tl; if( ra==NodeManager::currentNM()->mkConst(true) ){ long rr = range.getConst<Rational>().getNumerator().getLong()+1; Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl; |