From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 9 Mar 2020 05:15:09 +0000 (-0500)
Subject: Rewrite again full for DIV rewrite (#3945)
X-Git-Tag: cvc5-1.0.0~3550
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e3110121a3f19ba1594a9b54f7f332804fd2e2af;p=cvc5.git

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 4f93ba745..222b63db5 100644
--- 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 3bcbfa859..5ef9f9f6c 100644
--- 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
index 000000000..78035790b
--- /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)