From 2771a78471f42951a01a269e4ea8b993d3807533 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Fri, 29 Oct 2010 15:51:25 +0000
Subject: [PATCH] Fixes RowVector::has().

---
 src/theory/arith/row_vector.h | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h
index 2c88721ea..d68f8bc30 100644
--- 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);
   }
 
   /**
-- 
2.30.2