From: Tim King <taking@cs.nyu.edu>
Date: Fri, 29 Oct 2010 15:51:25 +0000 (+0000)
Subject: Fixes RowVector::has().
X-Git-Tag: cvc5-1.0.0~8761
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2771a78471f42951a01a269e4ea8b993d3807533;p=cvc5.git

Fixes RowVector::has().
---

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);
   }
 
   /**