Fixing a soundness bug in arithmetic and a roubustness problem in rings.

diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
index d5dcae72633e82176998c30d6f6259c5217fd561..d3702ccd8017084396f07430bc1ff0c081b8d1a2 100644 (file)
--- a/src/theory/arith/arith_ite_utils.cpp
+++ b/src/theory/arith/arith_ite_utils.cpp
@@ -308,6 +308,9 @@ void ArithIteUtils::addImplications(Node x, Node y){
   // (=> (not x) y)
   // (=> (not y) x)
 
+  x = Rewriter::rewrite(x);
+  y = Rewriter::rewrite(y);
+
   Node xneg = x.negate();
   Node yneg = y.negate();
   d_implies[xneg].insert(y);
@@ -369,9 +372,21 @@ bool ArithIteUtils::solveBinOr(TNode binor){
   Assert(binor[0].getKind() ==  kind::EQUAL);
   Assert(binor[1].getKind() ==  kind::EQUAL);
 
+  //Node n = 
   Node n = applySubstitutions(binor);
+  if(n != binor){
+    n = Rewriter::rewrite(n);
+
+    if(!(n.getKind() == kind::OR &&
+        n.getNumChildren() == 2 &&
+        n[0].getKind() ==  kind::EQUAL &&
+        n[1].getKind() ==  kind::EQUAL)){
+      return false;
+    }
+  }
+
   Assert(n.getKind() == kind::OR);
-  Assert(binor.getNumChildren() == 2);
+  Assert(n.getNumChildren() == 2);
   TNode l = n[0];
   TNode r = n[1];
 
@@ -416,7 +431,7 @@ bool ArithIteUtils::solveBinOr(TNode binor){
 
         NodeManager* nm = NodeManager::currentNM();
 
-        Node cnd = findIteCnd(binor[0], binor[1]);
+        Node cnd = findIteCnd(l, r);
 
         Node sk = nm->mkSkolem("deor", nm->booleanType());
         Node ite = sk.iteNode(otherL, otherR);

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index b2eec924c662ccccd98484b2ee3b442eb786263c..0fa9e79f21e30058c995ea0b47b4a4af9742079b 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -2965,6 +2965,19 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){
         if(mipRes == MipClosed){
           d_likelyIntegerInfeasible = true;
           replayLog(approx);
+
+         if(!anyConflict()){
+           //start up simplex
+           d_partialModel.stopQueueingBoundCounts();
+           UpdateTrackingCallback utcb(&d_linEq);
+           d_partialModel.processBoundsQueue(utcb);
+           d_linEq.startTrackingBoundCounts();
+           //call simplex
+           solveRelaxationOrPanic(effortLevel);
+           // shutdown simplex
+           d_linEq.stopTrackingBoundCounts();
+           d_partialModel.startQueueingBoundCounts();
+         }
         }
         if(!(anyConflict() || !d_approxCuts.empty())){
           turnOffApproxFor(options::replayNumericFailurePenalty());