diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/quantifiers/bounded_integers.cpp | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 4 |
2 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 6b53612d7..3d5066c08 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -797,6 +797,7 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node Node l, u; getBoundValues( q, v, rsi, l, u ); if( l.isNull() || u.isNull() ){ + Trace("bound-int-warn") << "WARNING: Could not find integer bounds in model for " << v << " in " << q << std::endl; //failed, abort the iterator return false; }else{ @@ -824,6 +825,7 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node }else if( bvt==BOUND_SET_MEMBER ){ Node srv = getSetRangeValue( q, v, rsi ); if( srv.isNull() ){ + Trace("bound-int-warn") << "WARNING: Could not find set bound in model for " << v << " in " << q << std::endl; return false; }else{ Trace("bound-int-rsi") << "Bounded by set membership : " << srv << std::endl; diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 88b5f5fb1..b1cc9ed19 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -70,6 +70,7 @@ Node FirstOrderModel::getAssertedQuantifier( unsigned i, bool ordered ) { } } +//AJR : FIXME : this function is only used by bounded integers, can likely be removed. Node FirstOrderModel::getCurrentModelValue( Node n, bool partial ) { std::vector< Node > children; if( n.getNumChildren()>0 ){ @@ -92,7 +93,8 @@ Node FirstOrderModel::getCurrentModelValue( Node n, bool partial ) { return nn; } }else{ - return getRepresentative(n); + //return getRepresentative(n); + return getValue(n); } } |