Fixes RowVector::has().

diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h
index 2c88721eac6fab3fd53003a3f7002ab13ea64b5b..d68f8bc30ba23c0e21c27f57d2995a4861b1e4a4 100644 (file)
--- a/src/theory/arith/row_vector.h
+++ b/src/theory/arith/row_vector.h
@@ -104,8 +104,7 @@ public:
 
   /** Returns true if the variable is in the row. */
   bool has(ArithVar x_j) const{
-    NonZeroIterator lb = lower_bound(x_j);
-    return getArithVar(*lb) == x_j;
+    return std::binary_search(d_entries.begin(), d_entries.end(), make_pair(x_j,0), cmp);
   }
 
   /**