Partial merge of integers work; this is simple B&B and some pseudoboolean

infrastructure, and takes care not to affect CVC4's performance on LRA
benchmarks.

1 files changed, 6 insertions, 2 deletions

diff --git a/src/theory/arith/ordered_set.h b/src/theory/arith/ordered_set.h
index 43ccd7815..e44ba8687 100644
--- a/src/theory/arith/ordered_set.h
+++ b/src/theory/arith/ordered_set.h
@@ -53,14 +53,18 @@ public:
   void addLeq(TNode leq){
     Assert(leq.getKind() == kind::LEQ);
     Assert(rightHandRational(leq) == getValue());
-    Assert(!hasLeq());
+    // [MGD] With context-dependent pre-registration, we could get the
+    // same one twice
+    Assert(!hasLeq() || d_leq == leq);
     d_leq = leq;
   }
 
   void addGeq(TNode geq){
     Assert(geq.getKind() == kind::GEQ);
     Assert(rightHandRational(geq) == getValue());
-    Assert(!hasGeq());
+    // [MGD] With context-dependent pre-registration, we could get the
+    // same one twice
+    Assert(!hasGeq() || d_geq == geq);
     d_geq = geq;
   }