Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into master. See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled.

1 files changed, 1 insertions, 1 deletions

diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 3e4cb819b..8cf92d075 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -81,7 +81,7 @@ public:
   }
 
   ArithVar rowIndexToBasic(RowIndex rid) const {
-    Assert(rid < d_rowIndex2basic.size());
+    Assert(d_rowIndex2basic.isKey(rid));
     return d_rowIndex2basic[rid];
   }