Fix integer division rewrite (#3415)

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 6dd6ffd56cf77c772f6f9a74a543249495988b65..86e5b3195d27d8137630a4c4d83d937e4ebeea6e 100644 (file)
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -742,8 +742,10 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre){
     //   (mod x (- c)) ---> (mod x c)
     NodeManager* nm = NodeManager::currentNM();
     Node nn = nm->mkNode(k, t[0], nm->mkConst(-t[1].getConst<Rational>()));
-    Node ret = k == kind::INTS_DIVISION ? nm->mkNode(kind::UMINUS, nn) : nn;
-    return RewriteResponse(REWRITE_AGAIN, nn);
+    Node ret = (k == kind::INTS_DIVISION || k == kind::INTS_DIVISION_TOTAL)
+                   ? nm->mkNode(kind::UMINUS, nn)
+                   : nn;
+    return RewriteResponse(REWRITE_AGAIN, ret);
   }else if(dIsConstant && n.getKind() == kind::CONST_RATIONAL){
     Assert(d.getConst<Rational>().isIntegral());
     Assert(n.getConst<Rational>().isIntegral());

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 7c0ab47a0b4f1e210ca09c325aa806d2b39ecc35..c1264a122cc3fc6b2466e25f6def9a5cbd8b734e 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -26,6 +26,8 @@ set(regress_0_tests
   regress0/arith/integers/arith-int-042.cvc
   regress0/arith/integers/arith-int-042.min.cvc
   regress0/arith/issue1399.smt2
+  regress0/arith/issue3412.smt2
+  regress0/arith/issue3413.smt2
   regress0/arith/leq.01.smtv1.smt2
   regress0/arith/miplib.cvc
   regress0/arith/miplib2.cvc

diff --git a/test/regress/regress0/arith/issue3412.smt2 b/test/regress/regress0/arith/issue3412.smt2
new file mode 100644 (file)
index 0000000..7986590
--- /dev/null
+++ b/test/regress/regress0/arith/issue3412.smt2
@@ -0,0 +1,4 @@
+(set-logic QF_NIA)
+(assert (= (div 1 (- 1)) (- 1)))
+(set-info :status sat)
+(check-sat)

diff --git a/test/regress/regress0/arith/issue3413.smt2 b/test/regress/regress0/arith/issue3413.smt2
new file mode 100644 (file)
index 0000000..290850d
--- /dev/null
+++ b/test/regress/regress0/arith/issue3413.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_NIA)
+(declare-fun a () Int)
+(declare-fun e () Int)
+(declare-fun f () Bool)
+(assert (= (div a e) (- 1)))
+(assert (= f (not (= e (- 1)))))
+(assert (ite f false (= (div a (- 1)) (- 1))))
+(set-info :status sat)
+(check-sat)