Rewrite again full for DIV rewrite (#3945)

Fixes #3944.

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 4f93ba74595f8e80f176914c78129ebd6c9d7799..222b63db5978d84fde932c03a80fa4cda063ea42 100644 (file)
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -753,7 +753,7 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre){
     Node ret = (k == kind::INTS_DIVISION || k == kind::INTS_DIVISION_TOTAL)
                    ? nm->mkNode(kind::UMINUS, nn)
                    : nn;
-    return RewriteResponse(REWRITE_AGAIN, ret);
+    return RewriteResponse(REWRITE_AGAIN_FULL, ret);
   }
   else if (dIsConstant && n.getKind() == kind::CONST_RATIONAL)
   {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 3bcbfa859159e21fe915748194fdd44c3ac51110..5ef9f9f6c09e9f468abfbf49ef98f3846290a8d7 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1839,6 +1839,7 @@ set(regress_1_tests
   regress1/sygus/issue3649.sy
   regress1/sygus/issue3802-default-consts.sy
   regress1/sygus/issue3839-cond-rewrite.smt2
+  regress1/sygus/issue3944-div-rewrite.smt2
   regress1/sygus/large-const-simp.sy
   regress1/sygus/let-bug-simp.sy
   regress1/sygus/list-head-x.sy

diff --git a/test/regress/regress1/sygus/issue3944-div-rewrite.smt2 b/test/regress/regress1/sygus/issue3944-div-rewrite.smt2
new file mode 100644 (file)
index 0000000..7803579
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3944-div-rewrite.smt2
@@ -0,0 +1,11 @@
+; EXPECT: sat
+; COMMAND-LINE: --sygus-inference
+(set-logic ALL)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun c () Int)
+(declare-fun d () Int)
+(assert (= c d))
+(assert (> (+ a (div 0 b)) c))
+(assert (= b (- 1)))
+(check-sat)