From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 4 May 2022 01:25:04 +0000 (-0500)
Subject: Fix rewrite for to_real in division by zero (#8714)
X-Git-Tag: cvc5-1.0.1~177
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=299cf5548603cc81d86ca5af4ea171765e17f584;p=cvc5.git

Fix rewrite for to_real in division by zero (#8714)

Fixes #8712.
---

diff --git a/src/preprocessing/passes/learned_rewrite.cpp b/src/preprocessing/passes/learned_rewrite.cpp
index 8545e6a78..eaff69825 100644
--- a/src/preprocessing/passes/learned_rewrite.cpp
+++ b/src/preprocessing/passes/learned_rewrite.cpp
@@ -95,6 +95,9 @@ PreprocessingPassResult LearnedRewrite::applyInternal(
           atomu = l;
           originLit[l] = l;
         }
+        atomu = rewrite(atomu);
+        Trace("learned-rewrite-ll")
+            << "Add atom (rewritten): " << atomu << std::endl;
         binfer.add(atomu);
       }
       Trace("learned-rewrite-ll") << "- " << l << std::endl;
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 502b528b1..77507b1b0 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -531,7 +531,8 @@ RewriteResponse ArithRewriter::rewriteDiv(TNode t, bool pre)
       }
       else
       {
-        return RewriteResponse(REWRITE_DONE, t);
+        Node ret = nm->mkNode(t.getKind(), left, right);
+        return RewriteResponse(REWRITE_DONE, ret);
       }
     }
     Assert(den != Rational(0));
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 0c8b54bb2..13324b7a4 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -812,6 +812,7 @@ set(regress_0_tests
   regress0/nl/issue8691-msum-subtypes.smt2
   regress0/nl/issue8691-3-msum-subtypes.smt2
   regress0/nl/issue8692-idem-flatten.smt2
+  regress0/nl/issue8712-div-toreal-rew.smt2
   regress0/nl/lazard-spurious-root.smt2
   regress0/nl/magnitude-wrong-1020-m.smt2
   regress0/nl/mult-po.smt2
diff --git a/test/regress/cli/regress0/nl/issue8712-div-toreal-rew.smt2 b/test/regress/cli/regress0/nl/issue8712-div-toreal-rew.smt2
new file mode 100644
index 000000000..4f7cf85fc
--- /dev/null
+++ b/test/regress/cli/regress0/nl/issue8712-div-toreal-rew.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --learned-rewrite -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-const a Real)
+(declare-const b Int)
+(assert (> a (/ (to_real b) (to_real 0))))
+(check-sat)