More bug fixes for interval models.

1 files changed, 13 insertions, 1 deletions

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 60d62391b..be6844a1e 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -665,4 +665,16 @@ bool FirstOrderModelFmc::isInterval(Node n) {
 
 Node FirstOrderModelFmc::getInterval( Node lb, Node ub ){
   return NodeManager::currentNM()->mkNode( APPLY_UF, intervalOp, lb, ub );
-}
\ No newline at end of file
+}
+
+bool FirstOrderModelFmc::isInRange( Node v, Node i ) {
+  for( unsigned b=0; b<2; b++ ){
+    if( !isStar( i[b] ) ){
+      if( ( b==0 && i[b].getConst<Rational>() > v.getConst<Rational>() ) ||
+          ( b==1 && i[b].getConst<Rational>() <= v.getConst<Rational>() ) ){
+        return false;
+      }
+    }
+  }
+  return true;
+}