Fixes a sign bug in the DioSolver.

diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 613ce836867044c27a988c689c8b1d641a34e191..28fe86c70874a82a34562d282efc92c4e811a22f 100644 (file)
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -375,6 +375,7 @@ DioSolver::TrailIndex DioSolver::impliedGcdOfOne(){
 
     //For the rest of the equations keep reducing until the coefficient is one
     for(; iter != end; ++iter){
+      Debug("arith::dio") << "next round : " << currentCoeff << " " << currentGcd << endl;
       TrailIndex inQueue = *iter;
       Constant iqc = d_trail[inQueue].d_eq.getPolynomial().getCoefficient(vl);
       if(!iqc.isZero()){
@@ -385,9 +386,9 @@ DioSolver::TrailIndex DioSolver::impliedGcdOfOne(){
         // g = a*s + b*t
         Integer::extendedGcd(g, s, t, currentCoeff, inQueueCoeff);
 
-        Debug("arith::dio") << "extendedReduction" << endl;
+        Debug("arith::dio") << "extendedReduction : " << endl;
         Debug("arith::dio") << g << " = " << s <<"*"<< currentCoeff << " + " << t <<"*"<< inQueueCoeff << endl;
-        
+
         Assert(g <= currentGcd);
         if(g < currentGcd){
           if(s.sgn() == 0){
@@ -395,10 +396,10 @@ DioSolver::TrailIndex DioSolver::impliedGcdOfOne(){
             Assert(inQueueCoeff.divides(currentGcd));
             current = *iter;
             currentCoeff = inQueueCoeff;
-            currentGcd = inQueueCoeff;
+            currentGcd = inQueueCoeff.abs();
           }else{
+
             Debug("arith::dio") << "extendedReduction combine" << endl;
-          
             TrailIndex next = combineEqAtIndexes(current, s, inQueue, t);
 
             Assert(d_trail[next].d_eq.getPolynomial().getCoefficient(vl).getValue().getNumerator() == g);

diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
index 7136662e660fc0c86f351588fe548d40dd63c86c..28d116c4a21ec4e445dbbb95f2581457110cb869 100644 (file)
--- a/test/regress/regress0/arith/Makefile.am
+++ b/test/regress/regress0/arith/Makefile.am
@@ -19,7 +19,8 @@ TESTS =       \
        delta-minimized-row-vector-bug.smt \
        fuzz_3-eq.smt \
        leq.01.smt \
-       miplibtrick.smt
+       miplibtrick.smt \
+       problem__003.smt2
 
 EXTRA_DIST = $(TESTS)
 

diff --git a/test/regress/regress0/arith/problem__003.smt2 b/test/regress/regress0/arith/problem__003.smt2
new file mode 100644 (file)
index 0000000..7af727e
--- /dev/null
+++ b/test/regress/regress0/arith/problem__003.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_LIA)
+(set-info :source |
+Alberto Griggio
+
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "random")
+(set-info :status sat)
+(declare-fun x0 () Int)
+(declare-fun x1 () Int)
+(declare-fun x2 () Int)
+(declare-fun x3 () Int)
+(declare-fun x4 () Int)
+(declare-fun x5 () Int)
+(declare-fun x6 () Int)
+(declare-fun x7 () Int)
+(declare-fun x8 () Int)
+(declare-fun x9 () Int)
+(assert (let ((?v_3 (* 36 x4)) (?v_0 (* 37 x7)) (?v_21 (* 3 x1)) (?v_7 (* 1 x1)) (?v_2 (* 23 x0)) (?v_4 (* 37 x1)) (?v_23 (* 15 x8)) (?v_11 (* 24 x1)) (?v_14 (* 30 x5)) (?v_17 (* 31 x6)) (?v_19 (* 28 x5)) (?v_5 (* 26 x5)) (?v_12 (* 13 x5)) (?v_20 (* 5 x6)) (?v_1 (* (- 38) x0)) (?v_18 (* (- 33) x4)) (?v_22 (* (- 38) x1)) (?v_16 (* (- 24) x6)) (?v_6 (* (- 13) x1)) (?v_9 (* (- 8) x4)) (?v_13 (* (- 11) x9)) (?v_10 (* (- 6) x0)) (?v_15 (* (- 37) x7)) (?v_8 (* (- 3) x4))) (and (<= (+ (* 25 x2) (* 12 x8) (* 12 x7) ?v_3 (* (- 5) x6) (* (- 25) x7) (* 22 x5) (* 7 x6) (* (- 19) x5) (* 22 x8)) (- 4)) (<= (+ (* 16 x1) (* 27 x2) (* 36 x6) (* 0 x8) (* 18 x4) (* (- 6) x1) (* 3 x9) (* (- 31) x9) (* 8 x0) ?v_0) (- 39)) (<= (+ (* 22 x1) (* 14 x3) (* (- 1) x2) (* (- 29) x9) (* 25 x8) (* 27 x4) (* (- 8) x3) (* (- 17) x4) ?v_1 (* 7 x7)) (- 25)) (<= (+ (* 16 x2) (* 2 x5) (* (- 34) x8) (* 3 x7) ?v_21 (* (- 17) x9) (* (- 32) x4) (* (- 7) x9) (* (- 9) x2) (* 16 x8)) (- 39)) (<= (+ ?v_7 (* (- 8) x5) (* 6 x4) ?v_18 (* (- 37) x0) (* 16 x6) (* (- 12) x0) (* 22 x3) (* (- 36) x3) (* 36 x0)) 6) (<= (+ (* 9 x3) (* (- 36) x4) (* (- 32) x8) (* (- 16) x1) ?v_0 ?v_2 (* (- 6) x5) (* (- 31) x6) (* (- 5) x8) (* (- 15) x3)) (- 15)) (<= (+ (* 1 x8) (* (- 7) x6) ?v_4 (* 20 x2) ?v_1 (* 0 x0) (* (- 37) x8) (* 13 x3) (* (- 23) x7) (* 37 x9)) (- 14)) (<= (+ (* 34 x5) (* 10 x6) (* (- 3) x5) (* (- 38) x9) ?v_22 (* 19 x6) (* (- 39) x7) ?v_16 (* 12 x1) (* (- 3) x7)) 35) (<= (+ (* 20 x4) (* (- 39) x9) (* 24 x3) ?v_23 (* (- 18) x3) ?v_11 (* (- 23) x4) ?v_14 (* 11 x2) (* (- 1) x5)) (- 13)) (<= (+ (* 30 x9) ?v_17 (* 14 x2) ?v_6 (* (- 16) x8) (* 29 x1) (* (- 3) x6) ?v_9 (* (- 10) x8) ?v_19) (- 39)) (<= (+ (* 8 x4) (* 37 x2) ?v_13 (* 23 x2) ?v_2 (* (- 4) x1) (* 10 x5) (* (- 36) x0) (* (- 15) x0) (* (- 22) x3)) (- 24)) (<= (+ (* 38 x2) (* 23 x3) (* 12 x2) ?v_10 ?v_3 (* 29 x6) (* 4 x0) ?v_5 ?v_15 (* (- 10) x9)) 16) (<= (+ (* 31 x4) (* (- 26) x0) (* (- 19) x9) (* (- 21) x4) ?v_4 ?v_8 ?v_5 ?v_12 (* (- 20) x4) (* (- 31) x2)) (- 12)) (<= (+ (* 38 x9) (* (- 28) x1) (* 29 x0) (* 5 x1) (* (- 38) x8) ?v_6 (* (- 8) x2) ?v_20 (* 22 x7) (* (- 24) x9)) 10) (<= (+ ?v_7 ?v_8 (* 35 x5) (* 16 x3) (* 6 x7) ?v_9 (* (- 2) x3) (* (- 38) x5) ?v_10 (* (- 7) x4)) (- 29)) (<= (+ (* 11 x3) (* 5 x4) (* (- 2) x4) (* 37 x6) ?v_11 (* 0 x9) (* 25 x1) (* (- 3) x9) (* (- 33) x9) (* 19 x9)) (- 37)) (<= (+ ?v_12 (* 7 x4) ?v_13 ?v_14 (* (- 31) x0) (* (- 12) x6) (* (- 35) x0) (* 36 x2) (* (- 25) x3) ?v_15) (- 33)) (<= (+ (* 10 x4) ?v_16 (* 26 x6) ?v_17 ?v_18 (* (- 32) x5) (* 32 x2) (* 34 x8) (* 19 x1) ?v_1) (- 9)) (<= (+ ?v_12 (* (- 9) x3) (* (- 37) x3) (* 34 x4) (* 0 x1) ?v_19 (* 30 x6) (* (- 18) x4) (* 21 x5) (* (- 21) x9)) (- 9)) (<= (+ ?v_20 (* (- 30) x6) ?v_21 (* 9 x8) ?v_13 (* (- 28) x5) (* (- 14) x3) ?v_22 (* 5 x8) ?v_23) 35))))
+(check-sat)
+(exit)