Significant revision to theory/arith. The new draft has a lot of small bug fixes and organizational changes. The theory is now enabled to perform checking in the TheoryEngine. This draft can now solve 2 new regression tests test/regress/regress0/ineq_slack.smt and test/regress/regress0/ineq_basic.smt. There is also a small bug fix inside src/expr/attribute.h.

1 files changed, 2 insertions, 1 deletions

diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 10daa0c13..2ab94c195 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -196,7 +196,8 @@ public:
     //Assert(isAdmissableVariable(var));
     Assert(var.getAttribute(IsBasic()));
 
-    Assert(d_basicVars.find(var) != d_basicVars.end());
+    //The new basic variable cannot already be a basic variable
+    Assert(d_basicVars.find(var) == d_basicVars.end());
     d_basicVars.insert(var);
     d_rows[var] = new Row(var,sum);
   }