Last commit accidentally lacked r2778 and r2779 from integer2. I have manually brought these changes over. Changed the tests used by test/regress/regress0/arith/integers/Makefile.am to be 15 of the more interesting tests. Did a bit of cleanup on TheoryArith to eliminate a warning and remove dead code.

1 files changed, 4 insertions, 4 deletions

diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index dead34807..1e47d6cdd 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -238,7 +238,7 @@ void DioSolver::enqueueInputConstraints(){
     TrailIndex i = d_inputConstraints[curr].d_trailPos;
     TrailIndex j = applyAllSubstitutionsToIndex(i);
 
-    if(!(triviallySat(j)  || anyCoefficientExceedsMaximum(j))){
+    if(!triviallySat(j)){
       if(triviallyUnsat(j)){
         raiseConflict(j);
       }else{
@@ -247,7 +247,7 @@ void DioSolver::enqueueInputConstraints(){
         if(!inConflict()){
           if(triviallyUnsat(k)){
             raiseConflict(k);
-          }else if(!triviallySat(k)){
+          }else if(!(triviallySat(k) || anyCoefficientExceedsMaximum(k))){
             pushToQueueBack(k);
           }
         }
@@ -772,10 +772,10 @@ void DioSolver::subAndReduceCurrentFByIndex(DioSolver::SubIndex subIndex){
 
       if(triviallyUnsat(nextTI)){
         raiseConflict(nextTI);
-      }else if(!(triviallySat(nextTI) || anyCoefficientExceedsMaximum(nextTI))){
+      }else if(!triviallySat(nextTI)){
         TrailIndex nextNextTI = reduceByGCD(nextTI);
 
-        if(!inConflict()){
+        if(!(inConflict() || anyCoefficientExceedsMaximum(nextNextTI))){
           Assert(queueConditions(nextNextTI));
           d_currentF[writeIter] = nextNextTI;
           ++writeIter;