- This fixes a problem where simplex produced the same conflict in the single check call.

- This increases the number of substitutions that ppAssert can solve on integer equations.

1 files changed, 10 insertions, 1 deletions

diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 2e0a9d067..fe10ecc4a 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -403,6 +403,15 @@ public:
   bool isUpperBound() const{
     return d_type == UpperBound;
   }
+  bool isStrictUpperBound() const{
+    Assert(isUpperBound());
+    return getValue().infinitesimalSgn() < 0;
+  }
+
+  bool isStrictLowerBound() const{
+    Assert(isLowerBound());
+    return getValue().infinitesimalSgn() > 0;
+  }
 
   bool isSplit() const {
     return d_split;
@@ -422,7 +431,7 @@ public:
 
   /**
    * Light wrapper for calling setCanBePropagated(),
-   * on this and this-d_negation.
+   * on this and this->d_negation.
    */
   void setPreregistered(){
     setCanBePropagated();