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 8545e6a78fba5de6357877e36a771a457cebed99..eaff69825c7fdb752e712011f295e568c04a259b 100644 (file)
--- 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 502b528b1eb60795e040969c48e0db31c29285a4..77507b1b0dc525a1a28fe2b201f2bca1176c050c 100644 (file)
--- 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 0c8b54bb28189c72749eff7e14bea65ad5978b7c..13324b7a4263b505c86400a26538fc79a6d1fd27 100644 (file)
--- 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 (file)
index 0000000..4f7cf85
--- /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)